diff --git a/cryptol/REPL/Command.hs b/cryptol/REPL/Command.hs
index 4e5de69f..e5fa5600 100644
--- a/cryptol/REPL/Command.hs
+++ b/cryptol/REPL/Command.hs
@@ -325,22 +325,22 @@ proveCmd :: String -> REPL ()
 proveCmd str = do
   parseExpr <- replParseExpr str
   (expr, schema) <- replCheckExpr parseExpr
-  eenv <- getExtEnv
+  denv <- getDynEnv
   -- spexpr <- replSpecExpr expr
   EnvString proverName <- getUser "prover"
   EnvBool iteSolver <- getUser "iteSolver"
   EnvBool verbose <- getUser "debug"
-  liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose, str) (M.eeDecls eenv) (expr, schema)
+  liftModuleCmd $ Cryptol.Symbolic.prove (proverName, iteSolver, verbose, str) (M.deDecls denv) (expr, schema)
 
 satCmd :: String -> REPL ()
 satCmd str = do
   parseExpr <- replParseExpr str
   (expr, schema) <- replCheckExpr parseExpr
-  eenv <- getExtEnv
+  denv <- getDynEnv
   EnvString proverName <- getUser "prover"
   EnvBool iteSolver <- getUser "iteSolver"
   EnvBool verbose <- getUser "debug"
-  liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose, str) (M.eeDecls eenv) (expr, schema)
+  liftModuleCmd $ Cryptol.Symbolic.sat (proverName, iteSolver, verbose, str) (M.deDecls denv) (expr, schema)
 
 specializeCmd :: String -> REPL ()
 specializeCmd str = do
@@ -421,7 +421,7 @@ loadCmd path
         { lName = Just (T.mName m)
         , lPath = path
         }
-      setExtEnv mempty
+      setDynEnv mempty
 
 quitCmd :: REPL ()
 quitCmd  = stop
@@ -591,21 +591,22 @@ moduleCmdResult (res,ws0) = do
     Left err      -> raise (ModuleSystemError err)
 
 replCheckExpr :: P.Expr -> REPL (T.Expr,T.Schema)
-replCheckExpr e = do
-  eenv <- getExtEnv
-  liftModuleCmd $ M.checkExprWith eenv e
+replCheckExpr e = liftModuleCmd $ M.checkExpr e
 
 replCheckDecls :: [P.Decl] -> REPL [T.DeclGroup]
 replCheckDecls ds = do
   npds <- liftModuleCmd $ M.noPat ds
-  eenv <- getExtEnv
+  denv <- getDynEnv
   let dnames = M.namingEnv npds
   ne' <- M.travNamingEnv uniqify dnames
-  let eenv' = eenv { M.eeNames = ne' `M.shadowing` M.eeNames eenv }
-  dgs <- liftModuleCmd $ M.checkDeclsWith eenv' npds
-  -- only update the REPL environment after a successful rename + typecheck
-  setExtEnv eenv'
-  return dgs
+  let denv' = denv { M.deNames = ne' `M.shadowing` M.deNames denv }
+      undo exn = do
+        -- if typechecking fails, we want to revert changes to the
+        -- dynamic environment and reraise
+        setDynEnv denv
+        raise exn
+  setDynEnv denv'
+  catch (liftModuleCmd $ M.checkDecls npds) undo
 
 replSpecExpr :: T.Expr -> REPL T.Expr
 replSpecExpr e = liftModuleCmd $ S.specialize e
@@ -625,8 +626,7 @@ replEvalExpr str =
                let su = T.listSubst [ (T.tpVar a, t) | (a,t) <- tys ]
                return (def1, T.apSubst su (T.sType sig))
 
-     eenv <- getExtEnv
-     val <- liftModuleCmd (M.evalExprWith eenv def1)
+     val <- liftModuleCmd (M.evalExpr def1)
      whenDebug (io (putStrLn (dump def1)))
      return (val,ty)
   where
@@ -637,9 +637,7 @@ replEvalDecls :: String -> REPL ()
 replEvalDecls str = do
   decls <- replParseDecls str
   dgs <- replCheckDecls decls
-  eenv <- getExtEnv
-  eenv' <- liftModuleCmd (M.evalDeclsWith eenv dgs)
-  setExtEnv eenv'
+  liftModuleCmd (M.evalDecls dgs)
 
 replEdit :: String -> REPL Bool
 replEdit file = do
diff --git a/cryptol/REPL/Monad.hs b/cryptol/REPL/Monad.hs
index e5d24d01..682cab3e 100644
--- a/cryptol/REPL/Monad.hs
+++ b/cryptol/REPL/Monad.hs
@@ -23,7 +23,7 @@ module REPL.Monad (
 
     -- ** Environment
   , getModuleEnv, setModuleEnv
-  , getExtEnv, setExtEnv
+  , getDynEnv, setDynEnv
   , uniqify
   , getTSyns, getNewtypes, getVars
   , whenDebug
@@ -52,6 +52,7 @@ import Cryptol.Prims.Syntax(ECon(..),ppPrefix)
 import Cryptol.Eval (EvalError)
 import qualified Cryptol.ModuleSystem as M
 import qualified Cryptol.ModuleSystem.Base as M
+import qualified Cryptol.ModuleSystem.Env as M
 import qualified Cryptol.ModuleSystem.NamingEnv as M
 import Cryptol.Parser (ParseError,ppError)
 import Cryptol.Parser.NoInclude (IncludeError,ppIncludeError)
@@ -86,8 +87,6 @@ data RW = RW
   , eContinue   :: Bool
   , eIsBatch    :: Bool
   , eModuleEnv  :: M.ModuleEnv
-  , eExtEnv     :: M.ExtendedEnv
-  -- ^ The dynamic environment for new bindings, eg @:let@
   , eNameSupply :: Int
   , eUserEnv    :: UserEnv
   }
@@ -101,7 +100,6 @@ defaultRW isBatch = do
     , eContinue   = True
     , eIsBatch    = isBatch
     , eModuleEnv  = env
-    , eExtEnv     = mempty
     , eNameSupply = 0
     , eUserEnv    = mkUserEnv userOptions
     }
@@ -260,12 +258,12 @@ keepOne src as = case as of
 getVars :: REPL (Map.Map P.QName M.IfaceDecl)
 getVars  = do
   me <- getModuleEnv
-  eenv <- getExtEnv
+  denv <- getDynEnv
   -- the subtle part here is removing the #Uniq prefix from
   -- interactively-bound variables, and also excluding any that are
   -- shadowed and thus can no longer be referenced
   let decls = M.focusedEnv me
-      edecls = M.ifDecls (M.eeIfaceDecls eenv)
+      edecls = M.ifDecls (M.deIfaceDecls denv)
       -- is this QName something the user might actually type?
       isShadowed (qn@(P.QName (Just (P.ModName ['#':_])) name), _) =
           case Map.lookup localName neExprs of
@@ -273,7 +271,7 @@ getVars  = do
             Just uniqueNames -> isNamed uniqueNames
         where localName = P.QName Nothing name
               isNamed us = any (== qn) (map M.qname us)
-              neExprs = M.neExprs (M.eeNames eenv)
+              neExprs = M.neExprs (M.deNames denv)
       isShadowed _ = False
       unqual ((P.QName _ name), ifds) = (P.QName Nothing name, ifds)
       edecls' = Map.fromList
@@ -321,11 +319,13 @@ getModuleEnv  = eModuleEnv `fmap` getRW
 setModuleEnv :: M.ModuleEnv -> REPL ()
 setModuleEnv me = modifyRW_ (\rw -> rw { eModuleEnv = me })
 
-getExtEnv :: REPL M.ExtendedEnv
-getExtEnv  = eExtEnv `fmap` getRW
+getDynEnv :: REPL M.DynamicEnv
+getDynEnv  = (M.meDynEnv . eModuleEnv) `fmap` getRW
 
-setExtEnv :: M.ExtendedEnv -> REPL ()
-setExtEnv eenv = modifyRW_ (\rw -> rw { eExtEnv = eenv })
+setDynEnv :: M.DynamicEnv -> REPL ()
+setDynEnv denv = do
+  me <- getModuleEnv
+  setModuleEnv (me { M.meDynEnv = denv })
 
 -- | Given an existing qualified name, prefix it with a
 -- relatively-unique string. We make it unique by prefixing with a
diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs
index a687e280..2c99f532 100644
--- a/src/Cryptol/ModuleSystem.hs
+++ b/src/Cryptol/ModuleSystem.hs
@@ -9,16 +9,16 @@
 module Cryptol.ModuleSystem (
     -- * Module System
     ModuleEnv(..), initialModuleEnv
-  , ExtendedEnv(..)
+  , DynamicEnv(..)
   , ModuleError(..), ModuleWarning(..)
   , ModuleCmd, ModuleRes
   , findModule
   , loadModuleByPath
   , loadModule
-  , checkExprWith
-  , evalExprWith
-  , checkDeclsWith
-  , evalDeclsWith
+  , checkExpr
+  , evalExpr
+  , checkDecls
+  , evalDecls
   , noPat
   , focusedEnv
 
@@ -71,20 +71,20 @@ loadModule m env = runModuleM env $ do
 -- can extend dynamically outside of the context of a module.
 
 -- | Check the type of an expression.
-checkExprWith :: ExtendedEnv -> P.Expr -> ModuleCmd (T.Expr,T.Schema)
-checkExprWith eenv e env = runModuleM env (interactive (Base.checkExprWith eenv e))
+checkExpr :: P.Expr -> ModuleCmd (T.Expr,T.Schema)
+checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
 
 -- | Evaluate an expression.
-evalExprWith :: ExtendedEnv -> T.Expr -> ModuleCmd E.Value
-evalExprWith eenv e env = runModuleM env (interactive (Base.evalExprWith eenv e))
+evalExpr :: T.Expr -> ModuleCmd E.Value
+evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
 
 -- | Typecheck declarations.
-checkDeclsWith :: ExtendedEnv -> [P.Decl] -> ModuleCmd [T.DeclGroup]
-checkDeclsWith eenv ds env = runModuleM env (interactive (Base.checkDeclsWith eenv ds))
+checkDecls :: [P.Decl] -> ModuleCmd [T.DeclGroup]
+checkDecls ds env = runModuleM env (interactive (Base.checkDecls ds))
 
 -- | Evaluate declarations and add them to the extended environment.
-evalDeclsWith :: ExtendedEnv -> [T.DeclGroup] -> ModuleCmd ExtendedEnv
-evalDeclsWith eenv dgs env = runModuleM env (interactive (Base.evalDeclsWith eenv dgs))
+evalDecls :: [T.DeclGroup] -> ModuleCmd ()
+evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs))
 
 noPat :: RemovePatterns a => a -> ModuleCmd a
 noPat a env = runModuleM env (interactive (Base.noPat a))
diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs
index fb436f9f..e8090298 100644
--- a/src/Cryptol/ModuleSystem/Base.hs
+++ b/src/Cryptol/ModuleSystem/Base.hs
@@ -8,7 +8,7 @@
 
 module Cryptol.ModuleSystem.Base where
 
-import Cryptol.ModuleSystem.Env (ExtendedEnv(..))
+import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
 import Cryptol.ModuleSystem.Interface
 import Cryptol.ModuleSystem.Monad
 import qualified Cryptol.Eval                 as E
@@ -32,7 +32,7 @@ import Data.Foldable (foldMap)
 import Data.Function (on)
 import Data.List (nubBy)
 import Data.Maybe (mapMaybe,fromMaybe)
-import Data.Monoid ((<>), mconcat)
+import Data.Monoid ((<>))
 import System.Directory (doesFileExist)
 import System.FilePath (addExtension,joinPath,(</>))
 import qualified Data.Map as Map
@@ -67,14 +67,8 @@ renameModule m = do
 renameExpr :: P.Expr -> ModuleM P.Expr
 renameExpr e = do
   env <- getFocusedEnv
-  rename (R.namingEnv env) e
-
--- | Rename an expression in the context of the focused module and an
--- extended environment.
-renameExprWith :: ExtendedEnv -> P.Expr -> ModuleM P.Expr
-renameExprWith eenv e = do
-  env <- getFocusedEnv
-  rename (eeNames eenv `R.shadowing` R.namingEnv env) e
+  denv <- getDynEnv
+  rename (deNames denv `R.shadowing` R.namingEnv env) e
 
 -- NoPat -----------------------------------------------------------------------
 
@@ -228,36 +222,20 @@ loadDeps m
 checkExpr :: P.Expr -> ModuleM (T.Expr,T.Schema)
 checkExpr e = do
   npe <- noPat e
+  denv <- getDynEnv
   re  <- renameExpr npe
-  typecheck T.tcExpr re =<< getQualifiedEnv
-
--- | Typecheck a single expression in an extended environment.
-checkExprWith :: ExtendedEnv -> P.Expr -> ModuleM (T.Expr,T.Schema)
-checkExprWith eenv e = do
-  npe <- noPat e
-  re  <- renameExprWith eenv npe
   env <- getQualifiedEnv
-  let env' = env <> eeIfaceDecls eenv
+  let env' = env <> deIfaceDecls denv
   typecheck T.tcExpr re env'
 
-eeIfaceDecls :: ExtendedEnv -> IfaceDecls
-eeIfaceDecls EEnv { eeDecls = dgs } =
-  mconcat [ IfaceDecls
-            { ifTySyns   = Map.empty
-            , ifNewtypes = Map.empty
-            , ifDecls    = Map.singleton (ifDeclName ifd) [ifd]
-            }
-          | decl <- concatMap T.groupDecls dgs
-          , let ifd = mkIfaceDecl decl
-          ]
-
--- | Typecheck a group of declarations in an extended environment.
-checkDeclsWith :: ExtendedEnv -> [P.Decl] -> ModuleM [T.DeclGroup]
-checkDeclsWith eenv ds = do
+-- | Typecheck a group of declarations.
+checkDecls :: [P.Decl] -> ModuleM [T.DeclGroup]
+checkDecls ds = do
   -- nopat must already be run
-  rds <- rename (eeNames eenv) ds
+  denv <- getDynEnv
+  rds <- rename (deNames denv) ds
   env <- getQualifiedEnv
-  let env' = env <> eeIfaceDecls eenv
+  let env' = env <> deIfaceDecls denv
   typecheck T.tcDecls rds env'
 
 -- | Typecheck a module.
@@ -340,18 +318,15 @@ genInferInput r env = do
 evalExpr :: T.Expr -> ModuleM E.Value
 evalExpr e = do
   env <- getEvalEnv
-  return (E.evalExpr env e)
+  denv <- getDynEnv
+  return (E.evalExpr (env <> deEnv denv) e)
 
-evalExprWith :: ExtendedEnv -> T.Expr -> ModuleM E.Value
-evalExprWith eenv e = do
+evalDecls :: [T.DeclGroup] -> ModuleM ()
+evalDecls dgs = do
   env <- getEvalEnv
-  return (E.evalExpr (env <> eeEnv eenv) e)
-
--- | Evaluate typechecked declarations in an extended environment. The
--- result of this is a new environment whose 'EvalEnv' is extended
--- with the new declarations and their values.
-evalDeclsWith :: ExtendedEnv -> [T.DeclGroup] -> ModuleM ExtendedEnv
-evalDeclsWith eenv dgs = do
-  env <- getEvalEnv
-  let env' = env <> eeEnv eenv
-  return $ eenv { eeDecls = eeDecls eenv ++ dgs, eeEnv = E.evalDecls dgs env' }
+  denv <- getDynEnv
+  let env' = env <> deEnv denv
+      denv' = denv { deDecls = deDecls denv ++ dgs
+                   , deEnv = E.evalDecls dgs env'
+                   }
+  setDynEnv denv'
diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs
index 3c2e15f8..fe22290e 100644
--- a/src/Cryptol/ModuleSystem/Env.hs
+++ b/src/Cryptol/ModuleSystem/Env.hs
@@ -22,6 +22,7 @@ import qualified Cryptol.TypeCheck.AST as T
 import Control.Monad (guard)
 import Data.Foldable (fold)
 import Data.Function (on)
+import qualified Data.Map as Map
 import Data.Monoid ((<>), Monoid(..))
 import System.Environment.Executable(splitExecutablePath)
 import System.FilePath ((</>), normalise, joinPath, splitPath)
@@ -36,6 +37,7 @@ data ModuleEnv = ModuleEnv
   , meEvalEnv       :: EvalEnv
   , meFocusedModule :: Maybe ModName
   , meSearchPath    :: [FilePath]
+  , meDynEnv        :: DynamicEnv
   }
 
 initialModuleEnv :: IO ModuleEnv
@@ -49,6 +51,7 @@ initialModuleEnv  = do
     , meEvalEnv       = mempty
     , meFocusedModule = Nothing
     , meSearchPath    = [dataDir </> "lib", instDir </> "lib", "."]
+    , meDynEnv        = mempty
     }
 
 -- | Try to focus a loaded module in the module environment.
@@ -128,27 +131,43 @@ addLoadedModule tm lm
     , lmModule    = tm
     }
 
--- Extended Environments -------------------------------------------------------
+-- Dynamic Environments --------------------------------------------------------
 
 -- | Extra information we need to carry around to dynamically extend
 -- an environment outside the context of a single module. Particularly
 -- useful when dealing with interactive declarations as in @:let@ or
 -- @it@.
 
-data ExtendedEnv = EEnv
-  { eeNames :: R.NamingEnv
-  , eeDecls :: [T.DeclGroup]
-  , eeEnv   :: EvalEnv
+data DynamicEnv = DEnv
+  { deNames :: R.NamingEnv
+  , deDecls :: [T.DeclGroup]
+  , deEnv   :: EvalEnv
   }
 
-instance Monoid ExtendedEnv where
-  mempty = EEnv
-    { eeNames = mempty
-    , eeDecls = mempty
-    , eeEnv   = mempty
+instance Monoid DynamicEnv where
+  mempty = DEnv
+    { deNames = mempty
+    , deDecls = mempty
+    , deEnv   = mempty
     }
-  mappend ee1 ee2 = EEnv
-    { eeNames = eeNames ee1 <> eeNames ee2
-    , eeDecls = eeDecls ee1 <> eeDecls ee2
-    , eeEnv   = eeEnv   ee1 <> eeEnv   ee2
+  mappend de1 de2 = DEnv
+    { deNames = deNames de1 <> deNames de2
+    , deDecls = deDecls de1 <> deDecls de2
+    , deEnv   = deEnv   de1 <> deEnv   de2
     }
+
+-- | Build 'IfaceDecls' that correspond to all of the bindings in the
+-- dynamic environment.
+--
+-- XXX: if we ever add type synonyms or newtypes at the REPL, revisit
+-- this.
+deIfaceDecls :: DynamicEnv -> IfaceDecls
+deIfaceDecls DEnv { deDecls = dgs } =
+  mconcat [ IfaceDecls
+            { ifTySyns   = Map.empty
+            , ifNewtypes = Map.empty
+            , ifDecls    = Map.singleton (ifDeclName ifd) [ifd]
+            }
+          | decl <- concatMap T.groupDecls dgs
+          , let ifd = mkIfaceDecl decl
+          ]
diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs
index 07ad3acb..592ff0c6 100644
--- a/src/Cryptol/ModuleSystem/Monad.hs
+++ b/src/Cryptol/ModuleSystem/Monad.hs
@@ -328,3 +328,11 @@ getFocusedEnv  = ModuleT (focusedEnv `fmap` get)
 
 getQualifiedEnv :: ModuleM IfaceDecls
 getQualifiedEnv  = ModuleT (qualifiedEnv `fmap` get)
+
+getDynEnv :: ModuleM DynamicEnv
+getDynEnv  = ModuleT (meDynEnv `fmap` get)
+
+setDynEnv :: DynamicEnv -> ModuleM ()
+setDynEnv denv = ModuleT $ do
+  me <- get
+  set $! me { meDynEnv = denv }