src/Tools/induct.ML

--- a/src/Tools/induct.ML	Mon Aug 12 21:22:40 2019 +0200
+++ b/src/Tools/induct.ML	Tue Aug 13 10:27:21 2019 +0200
@@ -535,7 +535,7 @@
     end;
 
 fun cases_tac ctxt x1 x2 x3 x4 x5 =
-  Method.NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
+  NO_CONTEXT_TACTIC ctxt (cases_context_tactic x1 x2 x3 x4 x5);
 
 end;
 
@@ -828,10 +828,10 @@
 val induct_context_tactic = gen_induct_context_tactic I;
 
 fun gen_induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 x8 =
-  Method.NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
+  NO_CONTEXT_TACTIC ctxt (gen_induct_context_tactic x1 x2 x3 x4 x5 x6 x7 x8);
 
 fun induct_tac ctxt x1 x2 x3 x4 x5 x6 x7 =
-  Method.NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
+  NO_CONTEXT_TACTIC ctxt (induct_context_tactic x1 x2 x3 x4 x5 x6 x7);
 
 
 
@@ -882,7 +882,7 @@
     end);
 
 fun coinduct_tac ctxt x1 x2 x3 x4 x5 =
-  Method.NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
+  NO_CONTEXT_TACTIC ctxt (coinduct_context_tactic x1 x2 x3 x4 x5);
 
 end;