--- a/src/Pure/Isar/proof.ML Wed Feb 02 13:26:38 2000 +0100
+++ b/src/Pure/Isar/proof.ML Wed Feb 02 20:19:25 2000 +0100
@@ -380,18 +380,11 @@
|> Drule.forall_elim_vars 0
end;
-fun most_general_varify_tfrees thm =
- let
- val {hyps, prop, ...} = Thm.rep_thm thm;
- val frees = foldr Term.add_term_frees (prop :: hyps, []);
- val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
- in thm |> Thm.varifyT' leave_tfrees end;
-
fun export fixes casms thm =
thm
|> Drule.implies_intr_list casms
|> varify_frees fixes
- |> most_general_varify_tfrees;
+ |> ProofContext.most_general_varify_tfrees;
fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
| diff_context inner (Some outer) =
@@ -476,7 +469,7 @@
err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
else if not (t aconv prop) then
err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
- else Drule.forall_elim_vars (maxidx + 1) thm
+ else thm |> Drule.forall_elim_vars (maxidx + 1) |> ProofContext.most_general_varify_tfrees
end;
--- a/src/Pure/Isar/proof_context.ML Wed Feb 02 13:26:38 2000 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Feb 02 20:19:25 2000 +0100
@@ -60,6 +60,7 @@
-> (thm list * context attribute list) list -> context -> context * (string * thm list)
val assumptions: context -> (cterm * ((int -> tactic) * (int -> tactic))) list
val fixed_names: context -> string list
+ val most_general_varify_tfrees: thm -> thm
val assume: ((int -> tactic) * (int -> tactic))
-> (string * context attribute list * (string * (string list * string list)) list) list
-> context -> context * ((string * thm list) list * thm list)
@@ -705,6 +706,14 @@
(* assume *)
+fun most_general_varify_tfrees thm =
+ let
+ val {hyps, prop, ...} = Thm.rep_thm thm;
+ val frees = foldr Term.add_term_frees (prop :: hyps, []);
+ val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
+ in thm |> Thm.varifyT' leave_tfrees end;
+
+
local
fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) =
@@ -713,7 +722,8 @@
val cprops = map (Thm.cterm_of (sign_of ctxt')) props;
val cprops_tac = map (rpair tac) cprops;
- val asms = map (Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
+ val asms =
+ map (most_general_varify_tfrees o Drule.forall_elim_vars 0 o Drule.assume_goal) cprops;
val ths = map (fn th => ([th], [])) asms;
val (ctxt'', (_, thms)) =