diff --git a/cryptol.cabal b/cryptol.cabal
index 479577f06..12824099f 100644
--- a/cryptol.cabal
+++ b/cryptol.cabal
@@ -66,6 +66,7 @@ library
                        random            >= 1.0.1,
                        sbv               >= 8.6,
                        simple-smt        >= 0.7.1,
+                       stm               >= 2.4,
                        strict,
                        text              >= 1.1,
                        tf-random         >= 0.5,
diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs
index 624ebdd13..eaa2c6e76 100644
--- a/src/Cryptol/Eval/Concrete.hs
+++ b/src/Cryptol/Eval/Concrete.hs
@@ -20,7 +20,7 @@
 {-# LANGUAGE ViewPatterns #-}
 module Cryptol.Eval.Concrete
   ( module Cryptol.Eval.Concrete.Value
-  , evalPrim
+  , primTable
   , toExpr
   ) where
 
@@ -131,11 +131,8 @@ floatToExpr prims eT pT f =
 
 -- Primitives ------------------------------------------------------------------
 
-evalPrim :: PrimIdent -> Maybe Value
-evalPrim prim = Map.lookup prim primTable
-
-primTable :: Map.Map PrimIdent Value
-primTable = let sym = Concrete in
+primTable :: EvalOpts -> Map.Map PrimIdent Value
+primTable eOpts = let sym = Concrete in
   Map.union (floatPrims sym) $
   Map.fromList $ map (\(n, v) -> (prelPrim n, v))
 
@@ -324,7 +321,7 @@ primTable = let sym = Concrete in
                       lam $ \x -> return $
                       lam $ \y -> do
                          msg <- valueToString sym =<< s
-                         EvalOpts { evalPPOpts, evalLogger } <- getEvalOpts
+                         let EvalOpts { evalPPOpts, evalLogger } = eOpts
                          doc <- ppValue sym evalPPOpts =<< x
                          yv <- y
                          io $ logPrint evalLogger
diff --git a/src/Cryptol/Eval/Monad.hs b/src/Cryptol/Eval/Monad.hs
index c12a5561a..0991ec01b 100644
--- a/src/Cryptol/Eval/Monad.hs
+++ b/src/Cryptol/Eval/Monad.hs
@@ -9,6 +9,7 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
 
 module Cryptol.Eval.Monad
@@ -16,7 +17,6 @@ module Cryptol.Eval.Monad
   Eval(..)
 , runEval
 , EvalOpts(..)
-, getEvalOpts
 , PPOpts(..)
 , PPFloatFormat(..)
 , PPFloatExp(..)
@@ -26,6 +26,7 @@ module Cryptol.Eval.Monad
 , ready
 , blackhole
 , evalSpark
+, maybeReady
   -- * Error reporting
 , Unsupported(..)
 , EvalError(..)
@@ -34,13 +35,13 @@ module Cryptol.Eval.Monad
 , typeCannotBeDemoted
 ) where
 
-import           Control.Concurrent.Async
-import           Control.DeepSeq
+import           Control.Concurrent
+import           Control.Concurrent.STM
+
 import           Control.Monad
 import qualified Control.Monad.Fail as Fail
 import           Control.Monad.Fix
 import           Control.Monad.IO.Class
-import           Data.IORef
 import           Data.Typeable (Typeable)
 import qualified Control.Exception as X
 
@@ -85,23 +86,69 @@ data EvalOpts = EvalOpts
   , evalPPOpts :: PPOpts    -- ^ How to pretty print things.
   }
 
-
 -- | The monad for Cryptol evaluation.
+--   A computation is either "ready", which means it represents
+--   only trivial computation, or is an "eval" action which must
+--   be computed to get the answer, or it is a "thunk", which
+--   represents a delayed, shared computation.
 data Eval a
    = Ready !a
-   | Thunk !(EvalOpts -> IO a)
-
+   | Eval !(IO a)
+   | Thunk !(TVar (ThunkState a))
+
+-- | This datastructure tracks the lifecycle of a thunk.
+--
+--   Thunks are used for basically three use cases.  First,
+--   we use thunks to preserve sharing.  Basically every
+--   cryptol expression that is bound to a name, and is not
+--   already obviously a value (and in a few other places as
+--   well) will get turned into a thunk in order to avoid
+--   recomputations.  These thunks will start in the `Unforced`
+--   state, and have a backup computation that just raises
+--   the `LoopError` exception.
+--
+--   Secondly, thunks are used to cut cycles when evaluating
+--   recursive definition groups.  Every named clause in a
+--   recursive definition is thunked so that the value can appear
+--   in its definition.  Such thunks start in the `Void` state,
+--   as they must exist before we have a definition to assign them.
+--   Forcing a thunk in the `Void` state is a programmer error (panic).
+--   Once the body of a definition is ready, we replace the
+--   thunk with the relevant computation, going to the `Unforced` state.
+--
+--   In the third case, we are using thunks to provide an optimistic
+--   shortcut for evaluation.  In these cases we first try to run a
+--   computation that is stricter than the semantics actually allows.
+--   If it succeeds, all is well an we continue.  However, if it tight
+--   loops, we fall back on a lazier (and generally more expensive)
+--   version, which is the "backup" computation referred to above.
 data ThunkState a
-  = Unforced        -- ^ This thunk has not yet been forced
-  | BlackHole       -- ^ This thunk is currently being evaluated
-  | Forced !(Either EvalError a)
-    -- ^ This thunk has previously been forced,
-    -- and has the given value, or evaluation resulted in an error.
-
-
--- | Access the evaluation options.
-getEvalOpts :: Eval EvalOpts
-getEvalOpts = Thunk pure
+  = Void !String
+       -- ^ This thunk has not yet been initialized
+  | Unforced !(IO a) !(IO a)
+       -- ^ This thunk has not yet been forced.  We keep track of the "main"
+       --   computation to run and a "backup" computation to run if we
+       --   detect a tight loop when evaluating the first one.
+  | UnderEvaluation !ThreadId !(IO a)
+       -- ^ This thunk is currently being evaluated by the thread with the given
+       --   thread ID.  We track the "backup" computation to run if we detect
+       --   a tight loop evaluating this thunk.  If the thunk is being evaluated
+       --   by some other thread, the current thread will await it's completion.
+  | ForcedErr !EvalError
+       -- ^ This thunk has been forced, and it's evaluation results in an exception
+  | Forced !a
+       -- ^ This thunk has been forced to the given value
+
+
+-- | Test if a value is "ready", which means that
+--   it requires no computation to return.
+maybeReady :: Eval a -> Eval (Maybe a)
+maybeReady (Ready a) = pure (Just a)
+maybeReady (Thunk tv) = Eval $
+  readTVarIO tv >>= \case
+     Forced a -> pure (Just a)
+     _ -> pure Nothing
+maybeReady (Eval _) = pure Nothing
 
 
 {-# INLINE delayFill #-}
@@ -114,11 +161,9 @@ delayFill ::
   Eval a {- ^ Computation to delay -} ->
   Eval a {- ^ Backup computation to run if a tight loop is detected -} ->
   Eval (Eval a)
-delayFill (Ready x) _ = Ready (Ready x)
-delayFill (Thunk x) retry = Thunk $ \opts -> do
-  r <- newIORef Unforced
-  return $ unDelay retry r (x opts)
-
+delayFill e@(Ready _) _  = return e
+delayFill e@(Thunk _) _  = return e
+delayFill (Eval x) backup = Eval (Thunk <$> newTVarIO (Unforced x (runEval backup)))
 
 -- | Begin executing the given operation in a separate thread,
 --   returning a thunk which will await the completion of
@@ -126,10 +171,54 @@ delayFill (Thunk x) retry = Thunk $ \opts -> do
 evalSpark ::
   Eval a ->
   Eval (Eval a)
-evalSpark (Ready x) = Ready (Ready x)
-evalSpark (Thunk x) = Thunk $ \opts ->
-  do a <- async (x opts)
-     return (Thunk $ \_ -> wait a)
+
+-- Ready computations need no additional evaluation.
+evalSpark e@(Ready _) = return e
+
+-- A thunked computation might already have
+-- been forced.  If so, return the result.  Otherwise,
+-- fork a thread to force this computation and return
+-- the thunk.
+evalSpark (Thunk tv)  = Eval $
+  readTVarIO tv >>= \case
+    Forced x     -> return (Ready x)
+    ForcedErr ex -> return (Eval (X.throwIO ex))
+    _ ->
+       do _ <- forkIO (sparkThunk tv)
+          return (Thunk tv)
+
+-- If the computation is nontrivial but not already a thunk,
+-- create a thunk and fork a thread to force it.
+evalSpark (Eval x) = Eval $
+  do tv <- newTVarIO (Unforced x (X.throwIO (LoopError "")))
+     _ <- forkIO (sparkThunk tv)
+     return (Thunk tv)
+
+
+-- | To the work of forcing a thunk. This is the worker computation
+--   that is foked off via @evalSpark@.
+sparkThunk :: TVar (ThunkState a) -> IO ()
+sparkThunk tv =
+  do tid <- myThreadId
+     -- Try to claim the thunk.  If it is still in the @Void@ state, wait
+     -- until it is in some other state.  If it is @Unforced@ claim the thunk.
+     -- Otherwise, it is already evaluated or under evaluation by another thread,
+     -- and we have no work to do.
+     st <- atomically $
+              do st <- readTVar tv
+                 case st of
+                   Void _ -> retry
+                   Unforced _ backup -> writeTVar tv (UnderEvaluation tid backup)
+                   _ -> return ()
+                 return st
+     -- If we successfully claimed the thunk to work on, run the computation and
+     -- update the thunk state with the result.
+     case st of
+       Unforced work _ ->
+         X.try work >>= \case
+           Left err -> atomically (writeTVar tv (ForcedErr err))
+           Right a  -> atomically (writeTVar tv (Forced a))
+       _ -> return ()
 
 
 -- | Produce a thunk value which can be filled with its associated computation
@@ -139,43 +228,76 @@ evalSpark (Thunk x) = Thunk $ \opts ->
 blackhole ::
   String {- ^ A name to associate with this thunk. -} ->
   Eval (Eval a, Eval a -> Eval ())
-blackhole msg = do
-  r <- io $ newIORef (fail msg)
-  let get = join (io $ readIORef r)
-  let set = io . writeIORef r
-  return (get, set)
-
-unDelay :: Eval a -> IORef (ThunkState a) -> IO a -> Eval a
-unDelay retry r x = do
-  rval <- io $ readIORef r
-  case rval of
-    Forced val -> io (toVal val)
-    BlackHole  ->
-      retry
-    Unforced -> io $ do
-      writeIORef r BlackHole
-      val <- X.try x
-      writeIORef r (Forced val)
-      toVal val
-
-  where
-  toVal mbV = case mbV of
-                Right a -> pure a
-                Left e  -> X.throwIO e
+blackhole msg = Eval $
+  do tv <- newTVarIO (Void msg)
+     let set (Ready x)  = io $ atomically (writeTVar tv (Forced x))
+         set m          = io $ atomically (writeTVar tv (Unforced (runEval m) (X.throwIO (LoopError msg))))
+     return (Thunk tv, set)
+
+-- | Force a thunk to get the result.
+unDelay :: TVar (ThunkState a) -> IO a
+unDelay tv =
+  -- First, check if the thunk is in an evaluated state,
+  -- and return the value if so.
+  readTVarIO tv >>= \case
+    Forced x -> pure x
+    ForcedErr e -> X.throwIO e
+    _ ->
+      -- Otherwise, try to claim the thunk to work on.
+      do tid <- myThreadId
+         res <- atomically $ do
+                  res <- readTVar tv
+                  case res of
+                    -- In this case, we claim the thunk.  Update the state to indicate
+                    -- that we are working on it.
+                    Unforced nm backup -> writeTVar tv (UnderEvaluation tid backup)
+
+                    -- In this case, the thunk is already being evaluated.  If it is
+                    -- under evaluation by this thread, we have to run the backup computation,
+                    -- and "consume" it by updating the backup computation to one that throws
+                    -- a loop error.  If some other thread is evaluating, reset the
+                    -- transaction to await completion of the thunk.
+                    UnderEvaluation t _
+                      | tid == t  -> writeTVar tv (UnderEvaluation tid (X.throwIO (LoopError "")))
+                      | otherwise -> retry -- wait, if some other thread is evaualting
+                    _ -> return ()
+
+                  -- Return the original thunk state so we can decide what work to do
+                  -- after the transaction completes.
+                  return res
+
+         -- helper for actually doing the work
+         let doWork work =
+               X.try work >>= \case
+                 Left ex -> do atomically (writeTVar tv (ForcedErr ex))
+                               X.throwIO ex
+                 Right a -> do atomically (writeTVar tv (Forced a))
+                               return a
+
+         -- Now, examine the thunk state and decide what to do.
+         case res of
+           Void msg -> evalPanic "unDelay" ["Thunk forced before it was initialized", msg]
+           Forced x -> pure x
+           ForcedErr e -> X.throwIO e
+           UnderEvaluation _ backup -> doWork backup -- this thread was already evaluating this thunk
+           Unforced work _ -> doWork work
 
 -- | Execute the given evaluation action.
-runEval :: EvalOpts -> Eval a -> IO a
-runEval _ (Ready a) = return a
-runEval opts (Thunk x) = x opts
+runEval :: Eval a -> IO a
+runEval (Ready a)  = return a
+runEval (Eval x)   = x
+runEval (Thunk tv) = unDelay tv
 
 {-# INLINE evalBind #-}
 evalBind :: Eval a -> (a -> Eval b) -> Eval b
 evalBind (Ready a) f  = f a
-evalBind (Thunk x) f  = Thunk $ \opts -> x opts >>= runEval opts . f
+evalBind (Eval x) f   = Eval (x >>= runEval . f)
+evalBind (Thunk x) f  = Eval (unDelay x >>= runEval . f)
 
 instance Functor Eval where
-  fmap f (Ready x) = Ready (f x)
-  fmap f (Thunk m) = Thunk $ \opts -> f <$> m opts
+  fmap f (Ready x)   = Ready (f x)
+  fmap f (Eval m)    = Eval (f <$> m)
+  fmap f (Thunk tv)  = Eval (f <$> unDelay tv)
   {-# INLINE fmap #-}
 
 instance Applicative Eval where
@@ -191,21 +313,17 @@ instance Monad Eval where
   {-# INLINE (>>=) #-}
 
 instance Fail.MonadFail Eval where
-  fail x = Thunk (\_ -> fail x)
+  fail x = Eval (fail x)
 
 instance MonadIO Eval where
   liftIO = io
 
-instance NFData a => NFData (Eval a) where
-  rnf (Ready a) = rnf a
-  rnf (Thunk _) = ()
-
 instance MonadFix Eval where
-  mfix f = Thunk $ \opts -> mfix (\x -> runEval opts (f x))
+  mfix f = Eval $ mfix (\x -> runEval (f x))
 
 -- | Lift an 'IO' computation into the 'Eval' monad.
 io :: IO a -> Eval a
-io m = Thunk (\_ -> m)
+io m = Eval m
 {-# INLINE io #-}
 
 
diff --git a/src/Cryptol/Eval/SBV.hs b/src/Cryptol/Eval/SBV.hs
index 991f6c6e9..ecc5e6998 100644
--- a/src/Cryptol/Eval/SBV.hs
+++ b/src/Cryptol/Eval/SBV.hs
@@ -18,7 +18,7 @@
 module Cryptol.Eval.SBV
   ( SBV(..), Value
   , SBVEval(..), SBVResult(..)
-  , evalPrim
+  , primTable
   , forallBV_, existsBV_
   , forallSBool_, existsSBool_
   , forallSInteger_, existsSInteger_
@@ -356,9 +356,6 @@ evalPanic cxt = panic ("[Symbolic]" ++ cxt)
 
 -- Primitives ------------------------------------------------------------------
 
-evalPrim :: PrimIdent -> Maybe Value
-evalPrim prim = Map.lookup prim primTable
-
 -- See also Cryptol.Eval.Concrete.primTable
 primTable :: Map.Map PrimIdent Value
 primTable  = let sym = SBV in
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
index a4ab764c7..ba0ac00f7 100644
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -205,13 +205,13 @@ memoMap x = do
 
   doEval cache i = do
     v <- lookupSeqMap x i
-    liftIO $ modifyIORef' cache (Map.insert i v)
+    liftIO $ atomicModifyIORef' cache (\m -> (Map.insert i v m, ()))
     return v
 
 -- | Apply the given evaluation function pointwise to the two given
 --   sequence maps.
 zipSeqMap ::
-  Backend sym => 
+  Backend sym =>
   (GenValue sym -> GenValue sym -> SEval sym (GenValue sym)) ->
   SeqMap sym ->
   SeqMap sym ->
@@ -221,7 +221,7 @@ zipSeqMap f x y =
 
 -- | Apply the given function to each value in the given sequence map
 mapSeqMap ::
-  Backend sym => 
+  Backend sym =>
   (GenValue sym -> SEval sym (GenValue sym)) ->
   SeqMap sym -> SEval sym (SeqMap sym)
 mapSeqMap f x =
@@ -281,7 +281,7 @@ indexWordValue sym (LargeBitsVal n xs) idx
 -- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the
 --   given bit value.
 updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym)
-updateWordValue sym (WordVal w) idx b 
+updateWordValue sym (WordVal w) idx b
    | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx
    | isReady sym b = WordVal <$> (wordUpdate sym w idx =<< b)
 
@@ -336,6 +336,7 @@ forceValue v = case v of
   VNumPoly _  -> return ()
 
 
+
 instance Backend sym => Show (GenValue sym) where
   show v = case v of
     VRecord fs -> "record:" ++ show (displayOrder fs)
diff --git a/src/Cryptol/Eval/What4.hs b/src/Cryptol/Eval/What4.hs
index de817d63a..262ceeb9e 100644
--- a/src/Cryptol/Eval/What4.hs
+++ b/src/Cryptol/Eval/What4.hs
@@ -13,7 +13,7 @@ module Cryptol.Eval.What4
   , W4Eval
   , w4Eval
   , Value
-  , evalPrim
+  , primTable
   ) where
 
 
@@ -31,10 +31,6 @@ import Cryptol.Eval.What4.Float(floatPrims)
 import Cryptol.Testing.Random( randomV )
 import Cryptol.Utils.Ident
 
-
-evalPrim :: W4.IsSymExprBuilder sym => sym -> PrimIdent -> Maybe (Value sym)
-evalPrim sym prim = Map.lookup prim (primTable sym)
-
 -- See also Cryptol.Prims.Eval.primTable
 primTable :: W4.IsSymExprBuilder sym => sym -> Map.Map PrimIdent (Value sym)
 primTable w4sym = let sym = What4 w4sym in
@@ -192,6 +188,3 @@ primTable w4sym = let sym = What4 w4sym in
          _ <- x
          y)
   ]
-
-
-
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index 2d48a0838..ab259afe3 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -202,7 +202,8 @@ doLoadModule isrc path fp pm0 =
      tcm <- optionalInstantiate =<< checkModule isrc path pm
 
      -- extend the eval env, unless a functor.
-     let ?evalPrim = Concrete.evalPrim
+     tbl <- Concrete.primTable <$> getEvalOpts
+     let ?evalPrim = \i -> Map.lookup i tbl
      unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)
      loadedModule path fp tcm
 
@@ -555,8 +556,9 @@ evalExpr e = do
   env <- getEvalEnv
   denv <- getDynEnv
   evopts <- getEvalOpts
-  let ?evalPrim = Concrete.evalPrim
-  io $ E.runEval evopts $ (E.evalExpr Concrete (env <> deEnv denv) e)
+  let tbl = Concrete.primTable evopts
+  let ?evalPrim = \i -> Map.lookup i tbl
+  io $ E.runEval $ (E.evalExpr Concrete (env <> deEnv denv) e)
 
 evalDecls :: [T.DeclGroup] -> ModuleM ()
 evalDecls dgs = do
@@ -564,8 +566,9 @@ evalDecls dgs = do
   denv <- getDynEnv
   evOpts <- getEvalOpts
   let env' = env <> deEnv denv
-  let ?evalPrim = Concrete.evalPrim
-  deEnv' <- io $ E.runEval evOpts $ E.evalDecls Concrete dgs env'
+  let tbl = Concrete.primTable evOpts
+  let ?evalPrim = \i -> Map.lookup i tbl
+  deEnv' <- io $ E.runEval $ E.evalDecls Concrete dgs env'
   let denv' = denv { deDecls = deDecls denv ++ dgs
                    , deEnv = deEnv'
                    }
diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs
index b3b12bfe5..3d9dc4d9e 100644
--- a/src/Cryptol/ModuleSystem/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Monad.hs
@@ -488,8 +488,7 @@ modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
 modifyEvalEnv f = ModuleT $ do
   env <- get
   let evalEnv = meEvalEnv env
-  evOpts <- unModuleT getEvalOpts
-  evalEnv' <- inBase $ E.runEval evOpts (f evalEnv)
+  evalEnv' <- inBase $ E.runEval (f evalEnv)
   set $! env { meEvalEnv = evalEnv' }
 
 getEvalEnv :: ModuleM EvalEnv
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
index e067e254a..b6858af5f 100644
--- a/src/Cryptol/REPL/Command.hs
+++ b/src/Cryptol/REPL/Command.hs
@@ -382,7 +382,6 @@ dumpTestsCmd :: FilePath -> String -> REPL ()
 dumpTestsCmd outFile str =
   do expr <- replParseExpr str
      (val, ty) <- replEvalExpr expr
-     evo <- getEvalOpts
      ppopts <- getPPValOpts
      testNum <- getKnownUser "tests" :: REPL Int
      g <- io newTFGen
@@ -390,7 +389,7 @@ dumpTestsCmd outFile str =
        case TestR.dumpableType ty of
          Nothing -> raise (TypeNotTestable ty)
          Just gens -> return gens
-     tests <- io $ TestR.returnTests g evo gens val testNum
+     tests <- io $ TestR.returnTests g gens val testNum
      out <- forM tests $
             \(args, x) ->
               do argOut <- mapM (rEval . E.ppValue Concrete ppopts) args
@@ -429,8 +428,7 @@ qcCmd qcMode str =
             let f _ [] = panic "Cryptol.REPL.Command"
                                     ["Exhaustive testing ran out of test cases"]
                 f _ (vs : vss1) = do
-                  evo <- getEvalOpts
-                  result <- io $ evalTest evo val vs
+                  result <- io $ evalTest val vs
                   return (result, vss1)
                 testSpec = TestSpec {
                     testFn = f
@@ -454,10 +452,9 @@ qcCmd qcMode str =
               Nothing   -> raise (TypeNotTestable ty)
               Just gens -> do
                 rPutStrLn "Using random testing."
-                evo <- getEvalOpts
                 let testSpec = TestSpec {
                         testFn = \sz' g ->
-                                      io $ TestR.runOneTest evo val gens sz' g
+                                      io $ TestR.runOneTest val gens sz' g
                       , testProp = str
                       , testTotal = toInteger testNum
                       , testPossible = sz
@@ -963,12 +960,10 @@ writeFileCmd file str = do
 
 
 rEval :: E.Eval a -> REPL a
-rEval m = do ev <- getEvalOpts
-             io (E.runEval ev m)
+rEval m = io (E.runEval m)
 
 rEvalRethrow :: E.Eval a -> REPL a
-rEvalRethrow m = do ev <- getEvalOpts
-                    io $ rethrowEvalError $ E.runEval ev m
+rEvalRethrow m = io $ rethrowEvalError $ E.runEval m
 
 reloadCmd :: REPL ()
 reloadCmd  = do
diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
index 3e8bb9e4a..c1165bc64 100644
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -33,6 +33,7 @@ import Control.Monad (replicateM, when, zipWithM, foldM, forM_)
 import Control.Monad.Writer (WriterT, runWriterT, tell, lift)
 import Data.List (genericLength)
 import Data.Maybe (fromMaybe)
+import qualified Data.Map as Map
 import qualified Control.Exception as X
 import System.Exit (ExitCode(ExitSuccess))
 
@@ -64,12 +65,12 @@ import           Cryptol.Utils.RecordMap
 import Prelude ()
 import Prelude.Compat
 
-doEval :: MonadIO m => Eval.EvalOpts -> Eval.Eval a -> m a
-doEval evo m = liftIO $ Eval.runEval evo m
+doEval :: MonadIO m => Eval.Eval a -> m a
+doEval m = liftIO $ Eval.runEval m
 
-doSBVEval :: MonadIO m => Eval.EvalOpts -> SBVEval a -> m (SBV.SVal, a)
-doSBVEval evo m =
-  (liftIO $ Eval.runEval evo (sbvEval m)) >>= \case
+doSBVEval :: MonadIO m => SBVEval a -> m (SBV.SVal, a)
+doSBVEval m =
+  (liftIO $ Eval.runEval (sbvEval m)) >>= \case
     SBVError err -> liftIO (X.throwIO err)
     SBVResult p x -> pure (p, x)
 
@@ -302,7 +303,8 @@ prepareQuery evo modEnv ProverCommand{..} =
            SafetyQuery -> \x y -> SBV.svOr (SBV.svNot x) y
            SatQuery _ -> \x y -> SBV.svAnd x y
 
-     let ?evalPrim = evalPrim
+     let tbl = primTable
+     let ?evalPrim = \i -> Map.lookup i tbl
      case predArgTypes pcQueryType pcSchema of
        Left msg -> return (Left msg)
        Right ts ->
@@ -314,7 +316,7 @@ prepareQuery evo modEnv ProverCommand{..} =
                  -- Run the main symbolic computation.  First we populate the
                  -- evaluation environment, then we compute the value, finally
                  -- we apply it to the symbolic inputs.
-                 (safety,b) <- doSBVEval evo $
+                 (safety,b) <- doSBVEval $
                      do env <- Eval.evalDecls SBV extDgs mempty
                         v <- Eval.evalExpr SBV env pcExpr
                         appliedVal <- foldM Eval.fromVFun v (map pure args)
@@ -341,12 +343,11 @@ prepareQuery evo modEnv ProverCommand{..} =
 -- | Turn the SMT results from SBV into a @ProverResult@ that is ready for the Cryptol REPL.
 --   There may be more than one result if we made a multi-sat query.
 processResults ::
-  Eval.EvalOpts ->
   ProverCommand ->
   [FinType] {- ^ Types of the symbolic inputs -} ->
   [SBV.SMTResult] {- ^ Results from the solver -} ->
   M.ModuleT IO ProverResult
-processResults evo ProverCommand{..} ts results =
+processResults ProverCommand{..} ts results =
  do let isSat = case pcQueryType of
           ProveQuery -> False
           SafetyQuery -> False
@@ -388,7 +389,7 @@ processResults evo ProverCommand{..} ts results =
         (vs, _) = parseValues ts cvs
         sattys = unFinType <$> ts
     satexprs <-
-      doEval evo (zipWithM (Concrete.toExpr prims) sattys vs)
+      doEval (zipWithM (Concrete.toExpr prims) sattys vs)
     case zip3 sattys <$> (sequence satexprs) <*> pure vs of
       Nothing ->
         panic "Cryptol.Symbolic.sat"
@@ -413,7 +414,7 @@ satProve proverCfg pc@ProverCommand {..} =
     Left msg -> return (Nothing, ProverError msg)
     Right (ts, q) ->
       do (firstProver, results) <- M.io (runProver proverCfg pc lPutStrLn q)
-         esatexprs <- processResults evo pc ts results
+         esatexprs <- processResults pc ts results
          return (firstProver, esatexprs)
 
 -- | Execute a symbolic ':prove' or ':sat' command when the prover is
diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs
index ccafb9786..dda542880 100644
--- a/src/Cryptol/Symbolic/What4.hs
+++ b/src/Cryptol/Symbolic/What4.hs
@@ -37,6 +37,7 @@ import System.IO (Handle)
 import Data.Time
 import Data.IORef
 import Data.List.NonEmpty (NonEmpty(..))
+import qualified Data.Map as Map
 import qualified Data.List.NonEmpty as NE
 import System.Exit
 
@@ -111,15 +112,15 @@ protectStack mkErr cmd modEnv =
         handler () = mkErr msg modEnv
 
 
-doEval :: MonadIO m => Eval.EvalOpts -> Eval.Eval a -> m a
-doEval evo m = liftIO $ Eval.runEval evo m
+doEval :: MonadIO m => Eval.Eval a -> m a
+doEval m = liftIO $ Eval.runEval m
 
 -- | Returns definitions, together with the value and it safety predicate.
 doW4Eval ::
   (W4.IsExprBuilder sym, MonadIO m) =>
-  sym -> Eval.EvalOpts -> W4Eval sym a -> m (W4Defs sym (W4.Pred sym, a))
-doW4Eval sym evo m =
-  do res <- liftIO $ Eval.runEval evo (w4Eval m sym)
+  sym -> W4Eval sym a -> m (W4Defs sym (W4.Pred sym, a))
+doW4Eval sym m =
+  do res <- liftIO $ Eval.runEval (w4Eval m sym)
      case w4Result res of
        W4Error err  -> liftIO (X.throwIO err)
        W4Result p x -> pure res { w4Result = (p,x) }
@@ -257,10 +258,10 @@ prepareQuery sym ProverCommand { .. } =
   simulate args =
     do let lPutStrLn = M.withLogger logPutStrLn
        when pcVerbose (lPutStrLn "Simulating...")
-       evo    <- M.getEvalOpts
        modEnv <- M.getModuleEnv
-       doW4Eval sym evo
-         do let ?evalPrim = evalPrim sym
+       doW4Eval sym
+         do let tbl = primTable sym
+            let ?evalPrim = \i -> Map.lookup i tbl
             let extDgs = allDeclGroups modEnv ++ pcExtraDecls
             env <- Eval.evalDecls (What4 sym) extDgs mempty
             v   <- Eval.evalExpr  (What4 sym) env    pcExpr
@@ -293,7 +294,7 @@ satProve solverCfg hashConsing ProverCommand {..} =
      query   <- prepareQuery sym ProverCommand { .. }
      primMap <- M.getPrimMap
      liftIO
-       do result <- runProver sym evo logData primMap query
+       do result <- runProver sym logData primMap query
           end <- getCurrentTime
           writeIORef pcProverStats (diffUTCTime end start)
           return result
@@ -313,21 +314,21 @@ satProve solverCfg hashConsing ProverCommand {..} =
       , logReason = "solver query"
       }
 
-  runProver sym evo logData primMap q =
+  runProver sym logData primMap q =
     case q of
       Left msg -> pure (Nothing, ProverError msg)
       Right (ts,args,safety,query) ->
         case pcQueryType of
           ProveQuery ->
-            singleQuery sym solverCfg evo primMap logData ts args
+            singleQuery sym solverCfg primMap logData ts args
                                                           (Just safety) query
 
           SafetyQuery ->
-            singleQuery sym solverCfg evo primMap logData ts args
+            singleQuery sym solverCfg primMap logData ts args
                                                           (Just safety) query
 
           SatQuery num ->
-            multiSATQuery sym solverCfg evo primMap logData ts args
+            multiSATQuery sym solverCfg primMap logData ts args
                                                             query num
 
 
@@ -375,7 +376,6 @@ multiSATQuery ::
   sym ~ W4.ExprBuilder t CryptolState fm =>
   sym ->
   W4ProverConfig ->
-  Eval.EvalOpts ->
   PrimMap ->
   W4.LogData ->
   [FinType] ->
@@ -383,19 +383,19 @@ multiSATQuery ::
   W4.Pred sym ->
   SatNum ->
   IO (Maybe String, ProverResult)
-multiSATQuery sym solverCfg evo primMap logData ts args query (SomeSat n) | n <= 1 =
-  singleQuery sym solverCfg evo primMap logData ts args Nothing query
+multiSATQuery sym solverCfg primMap logData ts args query (SomeSat n) | n <= 1 =
+  singleQuery sym solverCfg primMap logData ts args Nothing query
 
-multiSATQuery _sym (W4Portfolio _) _evo _primMap _logData _ts _args _query _satNum =
+multiSATQuery _sym (W4Portfolio _) _primMap _logData _ts _args _query _satNum =
   fail "What4 portfolio solver cannot be used for multi SAT queries"
 
-multiSATQuery sym (W4ProverConfig (AnAdapter adpt)) evo primMap logData ts args query satNum0 =
+multiSATQuery sym (W4ProverConfig (AnAdapter adpt)) primMap logData ts args query satNum0 =
   do pres <- W4.solver_adapter_check_sat adpt sym logData [query] $ \res ->
          case res of
            W4.Unknown -> return (Left (ProverError "Solver returned UNKNOWN"))
            W4.Unsat _ -> return (Left (ThmResult (map unFinType ts)))
            W4.Sat (evalFn,_) ->
-             do model <- computeModel evo primMap evalFn ts args
+             do model <- computeModel primMap evalFn ts args
                 blockingPred <- computeBlockingPred sym evalFn args
                 return (Right (model, blockingPred))
 
@@ -414,7 +414,7 @@ multiSATQuery sym (W4ProverConfig (AnAdapter adpt)) evo primMap logData ts args
            W4.Unknown -> return []
            W4.Unsat _ -> return []
            W4.Sat (evalFn,_) ->
-             do model <- computeModel evo primMap evalFn ts args
+             do model <- computeModel primMap evalFn ts args
                 return [model]
 
   computeMoreModels qs satNum =
@@ -423,7 +423,7 @@ multiSATQuery sym (W4ProverConfig (AnAdapter adpt)) evo primMap logData ts args
            W4.Unknown -> return Nothing
            W4.Unsat _ -> return Nothing
            W4.Sat (evalFn,_) ->
-             do model <- computeModel evo primMap evalFn ts args
+             do model <- computeModel primMap evalFn ts args
                 blockingPred <- computeBlockingPred sym evalFn args
                 return (Just (model, blockingPred))
 
@@ -436,7 +436,6 @@ singleQuery ::
   sym ~ W4.ExprBuilder t CryptolState fm =>
   sym ->
   W4ProverConfig ->
-  Eval.EvalOpts ->
   PrimMap ->
   W4.LogData ->
   [FinType] ->
@@ -445,8 +444,8 @@ singleQuery ::
   W4.Pred sym ->
   IO (Maybe String, ProverResult)
 
-singleQuery sym (W4Portfolio ps) evo primMap logData ts args msafe query =
-  do as <- mapM async [ singleQuery sym (W4ProverConfig p) evo primMap logData ts args msafe query
+singleQuery sym (W4Portfolio ps) primMap logData ts args msafe query =
+  do as <- mapM async [ singleQuery sym (W4ProverConfig p) primMap logData ts args msafe query
                       | p <- NE.toList ps
                       ]
      waitForResults [] as
@@ -465,13 +464,13 @@ singleQuery sym (W4Portfolio ps) evo primMap logData ts args msafe query =
           do forM_ others (\a -> X.throwTo (asyncThreadId a) ExitSuccess)
              return r
 
-singleQuery sym (W4ProverConfig (AnAdapter adpt)) evo primMap logData ts args msafe query =
+singleQuery sym (W4ProverConfig (AnAdapter adpt)) primMap logData ts args msafe query =
   do pres <- W4.solver_adapter_check_sat adpt sym logData [query] $ \res ->
          case res of
            W4.Unknown -> return (ProverError "Solver returned UNKNOWN")
            W4.Unsat _ -> return (ThmResult (map unFinType ts))
            W4.Sat (evalFn,_) ->
-             do model <- computeModel evo primMap evalFn ts args
+             do model <- computeModel primMap evalFn ts args
                 case msafe of
                   Just s ->
                     do s' <- W4.groundEval evalFn s
@@ -533,22 +532,21 @@ varBlockingPred sym evalFn v =
     VarRecord fs    -> computeBlockingPred sym evalFn (recordElements fs)
 
 computeModel ::
-  Eval.EvalOpts ->
   PrimMap ->
   W4.GroundEvalFn t ->
   [FinType] ->
   [VarShape (W4.ExprBuilder t CryptolState fm)] ->
   IO [(Type, Expr, Concrete.Value)]
-computeModel _ _ _ [] [] = return []
-computeModel evo primMap evalFn (t:ts) (v:vs) =
+computeModel _ _ [] [] = return []
+computeModel primMap evalFn (t:ts) (v:vs) =
   do v' <- varToConcreteValue evalFn v
      let t' = unFinType t
-     e <- doEval evo (Concrete.toExpr primMap t' v') >>= \case
+     e <- doEval (Concrete.toExpr primMap t' v') >>= \case
              Nothing -> panic "computeModel" ["could not compute counterexample expression"]
              Just e  -> pure e
-     zs <- computeModel evo primMap evalFn ts vs
+     zs <- computeModel primMap evalFn ts vs
      return ((t',e,v'):zs)
-computeModel _ _ _ _ _ = panic "computeModel" ["type/value list mismatch"]
+computeModel _ _ _ _ = panic "computeModel" ["type/value list mismatch"]
 
 
 data VarShape sym
diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs
index f07d5c950..51f55ced8 100644
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@@ -27,7 +27,7 @@ import System.Random.TF.Gen   (seedTFGen)
 
 import Cryptol.Eval.Backend   (Backend(..), SRational(..))
 import Cryptol.Eval.Concrete.Value
-import Cryptol.Eval.Monad     (ready,runEval,EvalOpts,Eval,EvalError(..))
+import Cryptol.Eval.Monad     (ready,runEval,Eval,EvalError(..))
 import Cryptol.Eval.Type      (TValue(..), tValTy)
 import Cryptol.Eval.Value     (GenValue(..),SeqMap(..), WordValue(..),
                                ppValue, defaultPPOpts, finiteSeqMap)
@@ -51,31 +51,29 @@ type Gen g x = Integer -> g -> (SEval x (GenValue x), g)
     the supplied value, otherwise we'll panic.
  -}
 runOneTest :: RandomGen g
-        => EvalOpts   -- ^ how to evaluate things
-        -> Value   -- ^ Function under test
+        => Value   -- ^ Function under test
         -> [Gen g Concrete] -- ^ Argument generators
         -> Integer -- ^ Size
         -> g
         -> IO (TestResult, g)
-runOneTest evOpts fun argGens sz g0 = do
+runOneTest fun argGens sz g0 = do
   let (args, g1) = foldr mkArg ([], g0) argGens
       mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
-  args' <- runEval evOpts (sequence args)
-  result <- evalTest evOpts fun args'
+  args' <- runEval (sequence args)
+  result <- evalTest fun args'
   return (result, g1)
 
 returnOneTest :: RandomGen g
-           => EvalOpts -- ^ How to evaluate things
-           -> Value    -- ^ Function to be used to calculate tests
+           => Value    -- ^ Function to be used to calculate tests
            -> [Gen g Concrete] -- ^ Argument generators
            -> Integer -- ^ Size
            -> g -- ^ Initial random state
            -> IO ([Value], Value, g) -- ^ Arguments, result, and new random state
-returnOneTest evOpts fun argGens sz g0 =
+returnOneTest fun argGens sz g0 =
   do let (args, g1) = foldr mkArg ([], g0) argGens
          mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
-     args' <- runEval evOpts (sequence args)
-     result <- runEval evOpts (go fun args')
+     args' <- runEval (sequence args)
+     result <- runEval (go fun args')
      return (args', result, g1)
    where
      go (VFun f) (v : vs) = join (go <$> (f (ready v)) <*> pure vs)
@@ -87,18 +85,17 @@ returnOneTest evOpts fun argGens sz g0 =
 -- | Return a collection of random tests.
 returnTests :: RandomGen g
          => g -- ^ The random generator state
-         -> EvalOpts -- ^ How to evaluate things
          -> [Gen g Concrete] -- ^ Generators for the function arguments
          -> Value -- ^ The function itself
          -> Int -- ^ How many tests?
          -> IO [([Value], Value)] -- ^ A list of pairs of random arguments and computed outputs
-returnTests g evo gens fun num = go gens g 0
+returnTests g gens fun num = go gens g 0
   where
     go args g0 n
       | n >= num = return []
       | otherwise =
         do let sz = toInteger (div (100 * (1 + n)) num)
-           (inputs, output, g1) <- returnOneTest evo fun args sz g0
+           (inputs, output, g1) <- returnOneTest fun args sz g0
            more <- go args g1 (n + 1)
            return ((inputs, output) : more)
 
@@ -330,11 +327,11 @@ isPass _    = False
 -- Note that this function assumes that the values come from a call to
 -- `testableType` (i.e., things are type-correct). We run in the IO
 -- monad in order to catch any @EvalError@s.
-evalTest :: EvalOpts -> Value -> [Value] -> IO TestResult
-evalTest evOpts v0 vs0 = run `X.catch` handle
+evalTest :: Value -> [Value] -> IO TestResult
+evalTest v0 vs0 = run `X.catch` handle
   where
     run = do
-      result <- runEval evOpts (go v0 vs0)
+      result <- runEval (go v0 vs0)
       if result
         then return Pass
         else return (FailFalse vs0)