# HG changeset patch
# User wenzelm
# Date 1272554123 -7200
# Node ID 6b56e679d9ffb0c08a081a1fd1433f1050d7ecf4
# Parent  79c1d2bbe5a969c8c8b3ea9134ea8f13a4facc92
adapted ProofContext.infer_type;

diff -r 79c1d2bbe5a9 -r 6b56e679d9ff src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Apr 29 16:55:22 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu Apr 29 17:15:23 2010 +0200
@@ -198,7 +198,7 @@
   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
 
 
@@ -430,7 +430,7 @@
           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;