most_general_varify_tfrees all results;
authorwenzelm
Wed Feb 02 20:19:25 2000 +0100 (2000-02-02)
changeset 818661ec7bedc717
parent 8185 59b62e8804b4
child 8187 535d6253f930
most_general_varify_tfrees all results;
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Feb 02 13:26:38 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Feb 02 20:19:25 2000 +0100
     1.3 @@ -380,18 +380,11 @@
     1.4      |> Drule.forall_elim_vars 0
     1.5    end;
     1.6  
     1.7 -fun most_general_varify_tfrees thm =
     1.8 -  let
     1.9 -    val {hyps, prop, ...} = Thm.rep_thm thm;
    1.10 -    val frees = foldr Term.add_term_frees (prop :: hyps, []);
    1.11 -    val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
    1.12 -  in thm |> Thm.varifyT' leave_tfrees end;
    1.13 -
    1.14  fun export fixes casms thm =
    1.15    thm
    1.16    |> Drule.implies_intr_list casms
    1.17    |> varify_frees fixes
    1.18 -  |> most_general_varify_tfrees;
    1.19 +  |> ProofContext.most_general_varify_tfrees;
    1.20  
    1.21  fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
    1.22    | diff_context inner (Some outer) =
    1.23 @@ -476,7 +469,7 @@
    1.24        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
    1.25      else if not (t aconv prop) then
    1.26        err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
    1.27 -    else Drule.forall_elim_vars (maxidx + 1) thm
    1.28 +    else thm |> Drule.forall_elim_vars (maxidx + 1) |> ProofContext.most_general_varify_tfrees
    1.29    end;
    1.30  
    1.31  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Wed Feb 02 13:26:38 2000 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Feb 02 20:19:25 2000 +0100
     2.3 @@ -60,6 +60,7 @@
     2.4      -> (thm list * context attribute list) list -> context -> context * (string * thm list)
     2.5    val assumptions: context -> (cterm * ((int -> tactic) * (int -> tactic))) list
     2.6    val fixed_names: context -> string list
     2.7 +  val most_general_varify_tfrees: thm -> thm
     2.8    val assume: ((int -> tactic) * (int -> tactic))
     2.9      -> (string * context attribute list * (string * (string list * string list)) list) list
    2.10      -> context -> context * ((string * thm list) list * thm list)
    2.11 @@ -705,6 +706,14 @@
    2.12  
    2.13  (* assume *)
    2.14  
    2.15 +fun most_general_varify_tfrees thm =
    2.16 +  let
    2.17 +    val {hyps, prop, ...} = Thm.rep_thm thm;
    2.18 +    val frees = foldr Term.add_term_frees (prop :: hyps, []);
    2.19 +    val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
    2.20 +  in thm |> Thm.varifyT' leave_tfrees end;
    2.21 +
    2.22 +
    2.23  local
    2.24  
    2.25  fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
    2.26 @@ -713,7 +722,8 @@
    2.27  
    2.28      val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
    2.29      val cprops_tac = map (rpair tac) cprops;
    2.30 -    val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
    2.31 +    val asms =
    2.32 +      map (most_general_varify_tfrees o Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
    2.33  
    2.34      val ths = map (fn th => ([th], [])) asms;
    2.35      val (ctxt'', (_, thms)) =