diff --git a/src/SAWScript/Prover/ABC.hs b/src/SAWScript/Prover/ABC.hs
index 50e9820731..a7a8bad4d2 100644
--- a/src/SAWScript/Prover/ABC.hs
+++ b/src/SAWScript/Prover/ABC.hs
@@ -4,7 +4,6 @@ module SAWScript.Prover.ABC (proveABC) where
 import qualified Data.AIG as AIG
 
 import           Verifier.SAW.SharedTerm
-import           Verifier.SAW.TypedTerm
 import           Verifier.SAW.FiniteValue
 import qualified Verifier.SAW.Simulator.BitBlast as BBSim
 
@@ -12,7 +11,7 @@ import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats (SolverStats, solverStats)
 import SAWScript.Prover.Rewrite(rewriteEqs)
 import SAWScript.Prover.Util
-         (liftCexBB, bindAllExts, checkBooleanSchema)
+         (liftCexBB, bindAllExts)
 
 -- | Bit-blast a proposition and check its validity using ABC.
 proveABC ::
@@ -23,9 +22,7 @@ proveABC ::
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveABC proxy sc goal =
   do t0 <- propToPredicate sc goal
-     TypedTerm schema t <-
-        (bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc)
-     checkBooleanSchema schema
+     t <- bindAllExts sc t0 >>= rewriteEqs sc
      BBSim.withBitBlastedPred proxy sc mempty t $
       \be lit0 shapes ->
          do let lit = AIG.not lit0
diff --git a/src/SAWScript/Prover/RME.hs b/src/SAWScript/Prover/RME.hs
index 6ee3f784e7..c4f8f0a5d5 100644
--- a/src/SAWScript/Prover/RME.hs
+++ b/src/SAWScript/Prover/RME.hs
@@ -7,7 +7,6 @@ import Verifier.SAW.FiniteValue
 
 import qualified Verifier.SAW.Simulator.RME as RME
 import qualified Verifier.SAW.Simulator.RME.Base as RME
-import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm)
 import Verifier.SAW.Recognizer(asPiList)
 
 import SAWScript.Proof(Prop, propToPredicate)
@@ -22,9 +21,7 @@ proveRME ::
   IO (Maybe [(String, FirstOrderValue)], SolverStats)
 proveRME sc goal =
   do t0 <- propToPredicate sc goal
-     TypedTerm schema t <-
-        bindAllExts sc t0 >>= rewriteEqs sc >>= mkTypedTerm sc
-     checkBooleanSchema schema
+     t <- bindAllExts sc t0 >>= rewriteEqs sc
      tp <- scWhnf sc =<< scTypeOf sc t
      let (args, _) = asPiList tp
          argNames = map fst args
diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs
index 83dd7b8347..4b5095970e 100644
--- a/src/SAWScript/Prover/SBV.hs
+++ b/src/SAWScript/Prover/SBV.hs
@@ -20,14 +20,11 @@ import qualified Verifier.SAW.Simulator.SBV as SBVSim
 
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
-import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm)
 import Verifier.SAW.Recognizer(asPi, asPiList)
 
 import SAWScript.Proof(Prop, propToPredicate)
 import SAWScript.Prover.SolverStats
 import SAWScript.Prover.Rewrite(rewriteEqs)
-import SAWScript.Prover.Util(checkBooleanSchema)
-
 
 
 -- | Bit-blast a proposition and check its validity using SBV.
@@ -93,10 +90,8 @@ prepNegatedSBV sc unints goal =
      let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
      exts <- filterM nonFun (getAllExts t0)
 
-     TypedTerm schema t' <-
-         scAbstractExts sc exts t0 >>= rewriteEqs sc >>= mkTypedTerm sc
+     t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
 
-     checkBooleanSchema schema
      (labels, lit) <- SBVSim.sbvSolve sc mempty unints t'
      let lit' = liftM SBV.svNot lit
      return (t', labels, lit')
diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs
index 772ec75c54..1945a97e11 100644
--- a/src/SAWScript/Prover/What4.hs
+++ b/src/SAWScript/Prover/What4.hs
@@ -13,13 +13,11 @@ import           Data.Maybe (catMaybes)
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.FiniteValue
 
-import Verifier.SAW.TypedTerm(TypedTerm(..), mkTypedTerm)
 import Verifier.SAW.Recognizer(asPi)
 
 import           SAWScript.Proof(Prop, propToPredicate)
 import           SAWScript.Prover.Rewrite(rewriteEqs)
 import           SAWScript.Prover.SolverStats
-import           SAWScript.Prover.Util
 
 import Data.Parameterized.Nonce
 
@@ -119,10 +117,8 @@ prepWhat4 sym sc unints t0 = do
   let nonFun e = fmap ((== Nothing) . asPi) (scWhnf sc (ecType e))
   exts <- filterM nonFun (getAllExts t0)
 
-  TypedTerm schema t' <-
-      scAbstractExts sc exts t0 >>= rewriteEqs sc >>= mkTypedTerm sc
+  t' <- scAbstractExts sc exts t0 >>= rewriteEqs sc
 
-  checkBooleanSchema schema
   (argNames, lit) <- W.w4Solve sym sc mempty unints t'
   return (t', argNames, lit)