# HG changeset patch
# User wenzelm
# Date 1438110641 -7200
# Node ID b4147850047307ecd9c0e039a9d271e33490a226
# Parent  4f58f3662e7d6b7175303c5586269914092f6198
clarified Variable.gen_all;
simplified Local_Defs.export: pointless partial application;

diff -r 4f58f3662e7d -r b41478500473 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Jul 28 20:59:39 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Jul 28 21:10:41 2015 +0200
@@ -129,32 +129,23 @@
   --------------
        B as
 *)
-fun export inner outer =    (*beware of closure sizes*)
+fun export inner outer th =
   let
-    val thy = Proof_Context.theory_of inner;
-    val maxidx0 = Variable.maxidx_of outer;
-    val exp = Assumption.export false inner outer;
-    val exp_term = Assumption.export_term inner outer;
-    val asms = Assumption.local_assms_of inner outer;
-  in
-    fn th =>
-      let
-        val th' = exp th;
-        val defs_asms = asms
-          |> filter_out (Drule.is_sort_constraint o Thm.term_of)
-          |> map (Thm.assume #> (fn asm =>
-            (case try (head_of_def o Thm.prop_of) asm of
-              NONE => (asm, false)
-            | SOME x =>
-                let val t = Free x in
-                  (case try exp_term t of
-                    NONE => (asm, false)
-                  | SOME u =>
-                      if t aconv u then (asm, false)
-                      else (Drule.abs_def (Drule.gen_all thy maxidx0 asm), true))
-                end)));
-      in (apply2 (map #1) (List.partition #2 defs_asms), th') end
-  end;
+    val defs_asms =
+      Assumption.local_assms_of inner outer
+      |> filter_out (Drule.is_sort_constraint o Thm.term_of)
+      |> map (Thm.assume #> (fn asm =>
+        (case try (head_of_def o Thm.prop_of) asm of
+          NONE => (asm, false)
+        | SOME x =>
+            let val t = Free x in
+              (case try (Assumption.export_term inner outer) t of
+                NONE => (asm, false)
+              | SOME u =>
+                  if t aconv u then (asm, false)
+                  else (Drule.abs_def (Variable.gen_all outer asm), true))
+            end)));
+  in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
 
 (*
   [xs, xs == as]
diff -r 4f58f3662e7d -r b41478500473 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 28 20:59:39 2015 +0200
+++ b/src/Pure/drule.ML	Tue Jul 28 21:10:41 2015 +0200
@@ -16,7 +16,6 @@
   val forall_intr_list: cterm list -> thm -> thm
   val forall_intr_vars: thm -> thm
   val forall_elim_list: cterm list -> thm -> thm
-  val gen_all: theory -> int -> thm -> thm
   val lift_all: Proof.context -> cterm -> thm -> thm
   val implies_elim_list: thm -> thm list -> thm
   val implies_intr_list: cterm list -> thm -> thm
@@ -53,6 +52,7 @@
 signature DRULE =
 sig
   include BASIC_DRULE
+  val outer_params: term -> (string * typ) list
   val generalize: string list * string list -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
@@ -182,15 +182,6 @@
   let val vs = Term.strip_all_vars t
   in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
 
-(*generalize outermost parameters*)
-fun gen_all thy maxidx0 th =
-  let
-    val maxidx = Thm.maxidx_thm th maxidx0;
-    val prop = Thm.prop_of th;
-    fun elim (x, T) =
-      Thm.forall_elim (Thm.global_cterm_of thy (Var ((x, maxidx + 1), T)));
-  in fold elim (outer_params prop) th end;
-
 (*lift vars wrt. outermost goal parameters
   -- reverses the effect of gen_all modulo higher-order unification*)
 fun lift_all ctxt raw_goal raw_th =
diff -r 4f58f3662e7d -r b41478500473 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Jul 28 20:59:39 2015 +0200
+++ b/src/Pure/variable.ML	Tue Jul 28 21:10:41 2015 +0200
@@ -498,7 +498,11 @@
 
 (** export -- generalize type/term variables (beware of closure sizes) **)
 
-fun gen_all ctxt = Drule.gen_all (Proof_Context.theory_of ctxt) (maxidx_of ctxt);
+fun gen_all ctxt th =
+  let
+    val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1;
+    fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T)));
+  in fold gen (Drule.outer_params (Thm.prop_of th)) th end;
 
 fun export_inst inner outer =
   let