diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 85f7521d2e..00124a490a 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -265,7 +265,7 @@ importType sc env ty =
           do tf' <- importTFun sc tf
              tyargs' <- traverse go tyargs
              scApplyAll sc tf' tyargs'
-        C.TError _k _msg ->
+        C.TError _k ->
           panic "importType TError" []
   where
     go = importType sc env
diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
index 5e26dc9a94..ea1cfa91eb 100644
--- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -250,15 +250,15 @@ runInferOutput :: TM.InferOutput a -> MM.ModuleM a
 runInferOutput out =
   case out of
 
-    TM.InferOK warns seeds supply o ->
+    TM.InferOK nm warns seeds supply o ->
       do MM.setNameSeeds seeds
          MM.setSupply supply
-         MM.typeCheckWarnings warns
+         MM.typeCheckWarnings nm warns
          return o
 
-    TM.InferFailed warns errs ->
-      do MM.typeCheckWarnings warns
-         MM.typeCheckingFailed errs
+    TM.InferFailed nm warns errs ->
+      do MM.typeCheckWarnings nm warns
+         MM.typeCheckingFailed nm errs
 
 -- Translate -------------------------------------------------------------------
 
@@ -642,7 +642,7 @@ moduleCmdResult (res, ws) = do
     suppressDefaulting :: MM.ModuleWarning -> MM.ModuleWarning
     suppressDefaulting w =
       case w of
-        MM.TypeCheckWarnings xs -> MM.TypeCheckWarnings (filter (notDefaulting . snd) xs)
+        MM.TypeCheckWarnings nm xs -> MM.TypeCheckWarnings nm (filter (notDefaulting . snd) xs)
         MM.RenamerWarnings xs -> MM.RenamerWarnings xs
 
     notDefaulting :: TE.Warning -> Bool