src/HOL/Statespace/state_space.ML

 
 fun mk_free ctxt name =
   if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
   then
     let val n' = lookupI (op =) (Variable.fixes_of ctxt) name
-    in SOME (Free (n',ProofContext.infer_type ctxt n')) end
+    in SOME (Free (n',ProofContext.infer_type ctxt (n', dummyT))) end
   else NONE
 
 
 fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name;
 fun get_comp ctxt name =

       let
         fun upd_prf ctxt =
           let
             fun upd (n,v) =
               let
-                val nT = ProofContext.infer_type (Local_Theory.target_of lthy) n
+                val nT = ProofContext.infer_type (Local_Theory.target_of lthy) (n, dummyT)
               in Context.proof_map
                   (update_declinfo (Morphism.term phi (Free (n,nT)),v))
               end;
           in ctxt |> fold upd updates end;