diff --git a/src/SAWScript/MGU.hs b/src/SAWScript/MGU.hs
index 47ab549f28..d9e34ce0fc 100644
--- a/src/SAWScript/MGU.hs
+++ b/src/SAWScript/MGU.hs
@@ -17,6 +17,7 @@ Stability   : provisional
 module SAWScript.MGU
        ( checkDecl
        , checkDeclGroup
+       , instantiateType
        ) where
 
 import SAWScript.AST
@@ -264,8 +265,12 @@ bindPatternSchema pat s@(Forall vs t) m =
 
 bindTypedef :: LName -> Type -> TI a -> TI a
 bindTypedef n t m =
-  TI $ local (\ro -> ro { typedefEnv = M.insert (getVal n) t $ typedefEnv ro })
-  $ unTI m
+  TI $
+  local
+    (\ro ->
+      let t' = instantiateType (typedefEnv ro) t
+      in  ro { typedefEnv = M.insert (getVal n) t' $ typedefEnv ro })
+    $ unTI m
 
 -- FIXME: This function may miss type variables that occur in the type
 -- of a binding that has been shadowed by another value with the same
@@ -382,10 +387,13 @@ instance Instantiate Type where
     TySkolemVar _ _ -> ty
     LType pos ty'   -> LType pos (instantiate nts ty')
 
+instantiateType :: Instantiate t => Map Name Type -> t -> t
+instantiateType tenv = instantiate (M.assocs tenv)
+
 instantiateM :: Instantiate t => t -> TI t
 instantiateM t = do
   s <- TI $ asks typedefEnv
-  return $ instantiate (M.assocs s) t
+  return $ instantiateType s t
 
 -- }}}
 
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 7875521e1e..f2a88fac9c 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -77,6 +77,7 @@ import qualified Text.LLVM.AST as LLVM (Type)
 import qualified Text.LLVM.PP as LLVM (ppType)
 import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.JavaPretty (prettyClass)
+import SAWScript.MGU (instantiateType)
 import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity(..))
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
@@ -504,7 +505,8 @@ extendLocal :: SS.LName -> Maybe SS.Schema -> Maybe String -> Value -> LocalEnv
 extendLocal x mt md v env = LocalLet x mt md v : env
 
 addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW
-addTypedef name ty rw = rw { rwTypedef = M.insert name ty (rwTypedef rw) }
+addTypedef name ty rw = rw { rwTypedef = M.insert name ty' (rwTypedef rw) }
+  where ty' = instantiateType (rwTypedef rw) ty
 
 mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW
 mergeLocalEnv sc env rw = foldrM addBinding rw env