src/HOL/Tools/coinduction.ML

       |> Seq.maps (fn st' =>
         CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
     end);
 
 fun coinduction_tac ctxt x1 x2 x3 x4 =
-  Method.NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
+  NO_CONTEXT_TACTIC ctxt (coinduction_context_tactic x1 x2 x3 x4);
 
 
 local
 
 val ruleN = "rule"