diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
index 57a910e2db..4e75424e4a 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -52,10 +52,9 @@ import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModu
 import SAWScript.Options (defaultOptions)
 import SAWScript.Position (Pos(..))
 import SAWScript.Prover.Rewrite (basic_ss)
-import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts)
+import SAWScript.Value (AIGProxy(..), BuiltinContext(..), JVMSetupM, LLVMCrucibleSetupM, TopLevelRO(..), TopLevelRW(..), defaultPPOpts, SAWSimpset)
 import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 import Verifier.SAW.CryptolEnv (initCryptolEnv, bindTypedTerm)
-import Verifier.SAW.Rewriter (Simpset)
 import qualified Cryptol.Utils.Ident as Cryptol
 
 import qualified Argo
@@ -275,7 +274,7 @@ data CrucibleSetupTypeRepr :: Type -> Type where
 
 data ServerVal
   = VTerm TypedTerm
-  | VSimpset Simpset
+  | VSimpset SAWSimpset
   | VType Cryptol.Schema
   | VCryptolModule CryptolModule -- from SAW, includes Term mappings
   | VJVMClass JSS.Class
@@ -305,7 +304,7 @@ class IsServerVal a where
 instance IsServerVal TypedTerm where
   toServerVal = VTerm
 
-instance IsServerVal Simpset where
+instance IsServerVal SAWSimpset where
   toServerVal = VSimpset
 
 instance IsServerVal Cryptol.Schema where
@@ -402,7 +401,7 @@ getLLVMMethodSpecIR n =
        VLLVMMethodSpecIR ir -> return ir
        _other -> Argo.raise (notAnLLVMMethodSpecIR n)
 
-getSimpset :: ServerName -> Argo.Command SAWState Simpset
+getSimpset :: ServerName -> Argo.Command SAWState SAWSimpset
 getSimpset n =
   do v <- getServerVal n
      case v of
diff --git a/saw-remote-api/src/SAWServer/ProofScript.hs b/saw-remote-api/src/SAWServer/ProofScript.hs
index 8293ef1ba1..d86b865d37 100644
--- a/saw-remote-api/src/SAWServer/ProofScript.hs
+++ b/saw-remote-api/src/SAWServer/ProofScript.hs
@@ -154,7 +154,7 @@ makeSimpset params = do
         v <- getServerVal n
         case v of
           VSimpset ss' -> return (merge ss ss')
-          VTerm t -> return (addSimp (ttTerm t) ss)
+          VTerm t -> return (addSimp (ttTerm t) Nothing ss) -- TODO! making rewrite rules from terms!
           _ -> Argo.raise (notASimpset n)
   ss <- foldM add emptySimpset (ssElements params)
   setServerVal (ssResult params) ss