most_general_varify_tfrees all results;

--- 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)) =