# HG changeset patch
# User wenzelm
# Date 1137351536 -3600
# Node ID 8ae076ee5e1954f251a0df1265f64a20967c911d
# Parent  2270e25e912882f66e0513e0f952e60b4a596e76
guess: used fixed inferred_type of vars;

diff -r 2270e25e9128 -r 8ae076ee5e19 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Jan 15 19:58:55 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Jan 15 19:58:56 2006 +0100
@@ -99,7 +99,6 @@
     val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     val xs = map #1 vars;
-    val Ts = map #2 vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -129,7 +128,7 @@
     fun after_qed _ =
       Proof.local_qed (NONE, false)
       #> Seq.map (`Proof.the_fact #-> (fn rule =>
-        Proof.fix_i (xs ~~ Ts)
+        Proof.fix_i (xs ~~ map #2 vars)
         #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
   in
     state
@@ -199,6 +198,10 @@
         commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
   in (xs' @ ys', rule') end;
 
+fun inferred_type (x, _, mx) ctxt =
+  let val ((_, T), ctxt') = ProofContext.inferred_type x ctxt
+  in ((x, SOME T, mx), ctxt') end;
+
 fun gen_guess prep_vars raw_vars int state =
   let
     val _ = Proof.assert_forward_or_chain state;
@@ -207,7 +210,7 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
-    val (vars, _) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
+    val (vars, _) = ctxt |> prep_vars (map Syntax.no_syn raw_vars) |-> fold_map inferred_type;
 
     fun check_result th =
       (case Thm.prems_of th of