guess: proper context for polymorphic parameters;
authorwenzelm
Tue Jul 04 19:49:55 2006 +0200 (2006-07-04)
changeset 20004e6d3f2b031e6
parent 20003 aac2c0d29751
child 20005 3fd6d57b16de
guess: proper context for polymorphic parameters;
tuned;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Tue Jul 04 19:49:54 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jul 04 19:49:55 2006 +0200
     1.3 @@ -74,8 +74,7 @@
     1.4      val bads = Term.fold_aterms (fn v as Free (x, _) =>
     1.5        if member (op =) parms x then insert (op aconv) v else I | _ => I) concl [];
     1.6  
     1.7 -    val thm' = thm |> Drule.implies_intr_protected cprops;
     1.8 -    val thm'' = thm' |> Thm.generalize ([], parms) (Thm.maxidx_of thm' + 1);
     1.9 +    val thm' = thm |> Drule.implies_intr_protected cprops |> Drule.generalize ([], parms);
    1.10      val elim_tacs = replicate (length cprops) (Tactic.etac Drule.protectI);
    1.11    in
    1.12      if not (null bads) then
    1.13 @@ -83,7 +82,7 @@
    1.14          space_implode " " (map (ProofContext.string_of_term ctxt) bads))
    1.15      else if not (ObjectLogic.is_judgment thy concl) then
    1.16        error "Conclusion in obtained context must be object-logic judgment"
    1.17 -    else (Tactic.rtac thm'' THEN' RANGE elim_tacs) 1 rule
    1.18 +    else (Tactic.rtac thm' THEN' RANGE elim_tacs) 1 rule
    1.19    end;
    1.20  
    1.21  
    1.22 @@ -209,14 +208,14 @@
    1.23      val vars' =
    1.24        map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
    1.25        (map snd vars @ replicate (length ys) NoSyn);
    1.26 -    val rule'' = Thm.generalize ([], [thesis_name]) (Thm.maxidx_of rule' + 1) rule';
    1.27 +    val rule'' = Drule.generalize ([], [thesis_name]) rule';
    1.28    in ((vars', rule''), ctxt') end;
    1.29  
    1.30  fun inferred_type (x, _, mx) ctxt =
    1.31    let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
    1.32    in ((x, T, mx), ctxt') end;
    1.33  
    1.34 -fun polymorphic (vars, ctxt) =
    1.35 +fun polymorphic ctxt vars =
    1.36    let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
    1.37    in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;
    1.38  
    1.39 @@ -228,7 +227,7 @@
    1.40      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
    1.41  
    1.42      val ((thesis_name, _), thesis) = bind_judgment ctxt AutoBind.thesisN;
    1.43 -    val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> polymorphic;
    1.44 +    val vars = ctxt |> prep_vars raw_vars |-> fold_map inferred_type |> fst |> polymorphic ctxt;
    1.45  
    1.46      fun check_result th =
    1.47        (case Thm.prems_of th of