src/Tools/induction.ML

--- a/src/Tools/induction.ML	Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Tools/induction.ML	Tue Aug 13 10:27:21 2019 +0200
@@ -47,7 +47,7 @@
       in ((cases', consumes), th) end);
 
 fun induction_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
-  Method.NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
+  NO_CONTEXT_TACTIC ctxt (induction_context_tactic x1 x2 x3 x4 x5 x6 x7);
 
 val _ =
   Theory.local_setup (Induct.gen_induct_setup \<^binding>\<open>induction\<close> induction_context_tactic);