tuned signature;
export: precomputed closure, no reference to contexts;

--- a/src/Pure/Isar/local_defs.ML	Sat Apr 14 00:46:20 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat Apr 14 00:46:21 2007 +0200
@@ -100,17 +100,22 @@
   end;
 
 
-(* specific export -- result based on educated guessing *)
+(* specific export -- result based on educated guessing (beware of closure sizes) *)
 
-fun export inner outer th =
+fun export inner outer =
   let
-    val th' = Assumption.export false inner outer th;
-    val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
-    val defs = Assumption.prems_of inner |> filter_out (fn prem =>
-      (case try (head_of_def o Thm.prop_of) prem of
-        SOME x => member (op =) still_fixed x
-      | NONE => true));
-  in (map Drule.abs_def defs, th') end;
+    val exp = Assumption.export false inner outer;
+    val prems = Assumption.prems_of inner;
+  in fn th =>
+    let
+      val th' = exp th;
+      val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
+      val defs = prems |> filter_out (fn prem =>
+        (case try (head_of_def o Thm.prop_of) prem of
+          SOME x => member (op =) still_fixed x
+        | NONE => true));
+    in (map Drule.abs_def defs, th') end
+  end;
 
 
 (* basic transitivity reasoning -- modulo beta-eta *)

--- a/src/Pure/variable.ML	Sat Apr 14 00:46:20 2007 +0200
+++ b/src/Pure/variable.ML	Sat Apr 14 00:46:21 2007 +0200
@@ -35,8 +35,6 @@
   val auto_fixes: term -> Proof.context -> Proof.context
   val variant_fixes: string list -> Proof.context -> string list * Proof.context
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
-  val export_inst: Proof.context -> Proof.context -> string list * string list
-  val exportT_inst: Proof.context -> Proof.context -> string list
   val export_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT_terms: Proof.context -> Proof.context -> term list -> term list
   val exportT: Proof.context -> Proof.context -> thm list -> thm list
@@ -161,10 +159,12 @@
 
 (* type occurrences *)
 
-val declare_type_occs = map_type_occs o fold_term_types
+val decl_type_occs = fold_term_types
   (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
     | _ => fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I));
 
+val declare_type_occs = map_type_occs o decl_type_occs;
+
 
 (* constraints *)
 
@@ -302,7 +302,7 @@
 
 
 
-(** export -- generalize type/term variables **)
+(** export -- generalize type/term variables (beware of closure sizes) **)
 
 fun export_inst inner outer =
   let
@@ -312,37 +312,48 @@
 
     val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
     val still_fixed = not o member (op =) gen_fixes;
-    val gen_fixesT =
+
+    val type_occs_inner = type_occs_of inner;
+    fun gen_fixesT ts =
       Symtab.fold (fn (a, xs) =>
         if declared_outer a orelse exists still_fixed xs
-        then I else cons a) (type_occs_of inner) [];
+        then I else cons a) (fold decl_type_occs ts type_occs_inner) [];
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
 
-fun exportT_terms inner outer ts =
-  map (TermSubst.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
-    (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
+fun exportT_terms inner outer =
+  let val mk_tfrees = exportT_inst inner outer in
+    fn ts => ts |> map
+      (TermSubst.generalize (mk_tfrees ts, [])
+        (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
+  end;
 
-fun export_terms inner outer ts =
-  map (TermSubst.generalize (export_inst (fold declare_type_occs ts inner) outer)
-    (fold Term.maxidx_term ts ~1 + 1)) ts;
+fun export_terms inner outer =
+  let val (mk_tfrees, tfrees) = export_inst inner outer in
+    fn ts => ts |> map
+      (TermSubst.generalize (mk_tfrees ts, tfrees)
+        (fold Term.maxidx_term ts ~1 + 1))
+  end;
 
 fun export_prf inner outer prf =
   let
-    val insts = export_inst (declare_prf prf inner) outer;
+    val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
+    val tfrees = mk_tfrees [];
     val idx = Proofterm.maxidx_proof prf ~1 + 1;
-    val gen_term = TermSubst.generalize_option insts idx;
-    val gen_typ = TermSubst.generalizeT_option (#1 insts) idx;
+    val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
+    val gen_typ = TermSubst.generalizeT_option tfrees idx;
   in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
 
-fun gen_export inst inner outer ths =
+
+fun gen_export (mk_tfrees, frees) ths =
   let
-    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths inner;
-  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths ~1 + 1)) ths end;
+    val tfrees = mk_tfrees (map Thm.full_prop_of ths);
+    val maxidx = fold Thm.maxidx_thm ths ~1;
+  in map (Thm.generalize (tfrees, frees) (maxidx + 1)) ths end;
 
-val exportT = gen_export (rpair [] oo exportT_inst);
-val export = gen_export export_inst;
+fun exportT inner outer = gen_export (exportT_inst inner outer, []);
+fun export inner outer = gen_export (export_inst inner outer);
 
 fun export_morphism inner outer =
   let