guess: used fixed inferred_type of vars;
authorwenzelm
Sun Jan 15 19:58:56 2006 +0100 (2006-01-15)
changeset 186938ae076ee5e19
parent 18692 2270e25e9128
child 18694 83f50ac6ddcb
guess: used fixed inferred_type of vars;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Sun Jan 15 19:58:55 2006 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Sun Jan 15 19:58:56 2006 +0100
     1.3 @@ -99,7 +99,6 @@
     1.4      val (vars, vars_ctxt) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
     1.5      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     1.6      val xs = map #1 vars;
     1.7 -    val Ts = map #2 vars;
     1.8  
     1.9      (*obtain asms*)
    1.10      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.11 @@ -129,7 +128,7 @@
    1.12      fun after_qed _ =
    1.13        Proof.local_qed (NONE, false)
    1.14        #> Seq.map (`Proof.the_fact #-> (fn rule =>
    1.15 -        Proof.fix_i (xs ~~ Ts)
    1.16 +        Proof.fix_i (xs ~~ map #2 vars)
    1.17          #> Proof.assm_i (K (obtain_export ctxt parms rule)) asms));
    1.18    in
    1.19      state
    1.20 @@ -199,6 +198,10 @@
    1.21          commas (map (string_of_typ o TVar) tvars @ map (string_of_term o Var) vars) ^ " in") rule';
    1.22    in (xs' @ ys', rule') end;
    1.23  
    1.24 +fun inferred_type (x, _, mx) ctxt =
    1.25 +  let val ((_, T), ctxt') = ProofContext.inferred_type x ctxt
    1.26 +  in ((x, SOME T, mx), ctxt') end;
    1.27 +
    1.28  fun gen_guess prep_vars raw_vars int state =
    1.29    let
    1.30      val _ = Proof.assert_forward_or_chain state;
    1.31 @@ -207,7 +210,7 @@
    1.32      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    1.33  
    1.34      val (thesis_var, thesis) = bind_judgment ctxt AutoBind.thesisN;
    1.35 -    val (vars, _) = prep_vars (map Syntax.no_syn raw_vars) ctxt;
    1.36 +    val (vars, _) = ctxt |> prep_vars (map Syntax.no_syn raw_vars) |-> fold_map inferred_type;
    1.37  
    1.38      fun check_result th =
    1.39        (case Thm.prems_of th of