--- a/src/Pure/drule.ML Tue Jul 28 20:15:19 2015 +0200
+++ b/src/Pure/drule.ML Tue Jul 28 20:59:39 2015 +0200
@@ -16,7 +16,7 @@
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: int -> 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
@@ -183,9 +183,8 @@
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
(*generalize outermost parameters*)
-fun gen_all maxidx0 th =
+fun gen_all thy maxidx0 th =
let
- val thy = Thm.theory_of_thm th;
val maxidx = Thm.maxidx_thm th maxidx0;
val prop = Thm.prop_of th;
fun elim (x, T) =