diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
index dcfec8152e..efb7bde929 100644
Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ
diff --git a/intTests/test0012_jss_aig/README b/intTests/test0012_jss_aig/README
index c2303dd0b6..54a7882964 100644
--- a/intTests/test0012_jss_aig/README
+++ b/intTests/test0012_jss_aig/README
@@ -4,10 +4,10 @@ The tests in 'test.saw' only make sense for the SAW backend; the
 default backend encodes the arguments and results in a different
 way.
 
-There used to be a bug in JSS and LSS where multiple AIG writes
-interacted, causing the number of input bits in the AIG to grow with
-each write. So in 'test.sh' we are careful to check that the number of
-input bits is always 16.
+There used to be a bug in JSS where multiple AIG writes interacted,
+causing the number of input bits in the AIG to grow with each write. So
+in 'test.sh' we are careful to check that the number of input bits is
+always 16.
 
 Besides checking predicates, where the input encoding does not matter,
 and the output is a single bit, we also check the input and output
diff --git a/intTests/test0015_sawscript_aig/README b/intTests/test0015_sawscript_aig/README
index e0c9b66d06..cc3c817597 100644
--- a/intTests/test0015_sawscript_aig/README
+++ b/intTests/test0015_sawscript_aig/README
@@ -3,9 +3,8 @@ Test AIG generation in SAWScript.
 These examples provide some documentation of the SAWScript AIG
 encoding.
 
-Note that, compared to LSS and JSS, the arguments here are reversed:
-for functions '\x -> \y -> e' the arguments are packed as 'x # y'
-here, but as 'y # x' for LSS and JSS. However, in LSS and JSS you
-don't actually write the arguments explicitly -- rather, open terms
-are closed over the symbolic variables in scope -- so I'm not sure the
-comparison is fair.
+Note that, compared to JSS, the arguments here are reversed: for
+functions '\x -> \y -> e' the arguments are packed as 'x # y' here, but
+as 'y # x' for JSS. However, in JSS you don't actually write the
+arguments explicitly -- rather, open terms are closed over the symbolic
+variables in scope -- so I'm not sure the comparison is fair.
diff --git a/intTests/test0015_sawscript_aig/test.saw b/intTests/test0015_sawscript_aig/test.saw
index f37a1694a1..74b83f4402 100644
--- a/intTests/test0015_sawscript_aig/test.saw
+++ b/intTests/test0015_sawscript_aig/test.saw
@@ -9,13 +9,12 @@ write_aig "tmp/yy.aig"    {{ \(x:[8]) -> \(y:[8]) -> y + y }};
 write_aig "tmp/2y.aig"    {{ \(x:[8]) -> \(y:[8]) -> 2 * y }};
 
 // The code below is very similar to '../test0012_jss_aig/test.saw'
-// and '../test0014_lss_aig/test.saw'.
 
 // Many of these Cryptol functions have types more specific than
 // necessary. The point is to document the behavior of SAWScript
 // AIG generation.
 let {{
-  // Arguments are reversed, compared to LSS and JSS.
+  // Arguments are reversed, compared to JSS.
 
   run_pred : ([16] -> [1]) -> [8] -> [8] -> [1]
   run_pred f x y = f (((zero # x) <<< 8) + (zero # y))
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index bd6244a6c8..ea06c1f450 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1969,9 +1969,7 @@ primitives = Map.fromList
     Current
     [ "Return a SetupValue representing the value of the initializer of a named"
     , "global. The String should be the name of a global value."
-    , "Note that initializing global variables may be unsound in the presence"
-    , "of compositional verification (see GaloisInc/saw-script#203)."
-    ] -- TODO: There should be a section in the manual about global-unsoundness.
+    ]
 
   , prim "crucible_term"
     "Term -> SetupValue"
diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs
index f550eb02c2..3305e7161b 100644
--- a/src/SAWScript/MGU.hs
+++ b/src/SAWScript/MGU.hs
@@ -473,7 +473,11 @@ inferE (ln, expr) = case expr of
     do env <- TI $ asks typeEnv
        case M.lookup x env of
          Nothing -> do
-           recordError $ "unbound variable: " ++ show x
+           recordError $ unlines
+             [ "Unbound variable: " ++ show x
+             , "Note that some built-in commands are available only after running"
+             , "either `enable_deprecated` or `enable_experimental`."
+             ]
            t <- newType
            return (Var x, t)
          Just (Forall as t) -> do