diff -r 88505460fde7 -r befdc10ebb42 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Jun 02 10:12:46 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue Jun 02 11:03:02 2015 +0200
@@ -65,7 +65,7 @@
   val partition_rules: thm -> thm list -> (string * thm list) list
   val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
   val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
-  val infer_intro_vars: thm -> int -> thm list -> term list list
+  val infer_intro_vars: theory -> thm -> int -> thm list -> term list list
 end;
 
 signature INDUCTIVE =
@@ -1132,9 +1132,8 @@
     (fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
 
 (* infer order of variables in intro rules from order of quantifiers in elim rule *)
-fun infer_intro_vars elim arity intros =
+fun infer_intro_vars thy elim arity intros =
   let
-    val thy = Thm.theory_of_thm elim;
     val _ :: cases = Thm.prems_of elim;
     val used = map (fst o fst) (Term.add_vars (Thm.prop_of elim) []);
     fun mtch (t, u) =