diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -395,7 +395,7 @@
           (fn {context = ctxt, prems} => EVERY
           [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac ctxt rews,
-           REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
+           REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
               DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
@@ -459,7 +459,7 @@
              etac elimR 1,
              ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
              rewrite_goals_tac ctxt rews,
-             REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
+             REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
                DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy