src/Tools/induct.ML

 (* make_cases *)
 
 fun make_cases is_open rule =
   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
 
-fun warn_open ctxt true =
-      legacy_feature ("open rule cases in proof method" ^ ContextPosition.str_of ctxt)
-  | warn_open _ false = ();
+fun warn_open true =
+      legacy_feature ("open rule cases in proof method" ^ Position.str_of (Position.thread_data ()))
+  | warn_open false = ();
 
 
 
 (** cases method **)
 

 
 in
 
 fun cases_tac ctxt is_open insts opt_rule facts =
   let
-    val _ = warn_open ctxt is_open;
+    val _ = warn_open is_open;
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     fun inst_rule r =
       if null insts then `RuleCases.get r

 
 in
 
 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
   let
-    val _ = warn_open ctxt is_open;
+    val _ = warn_open is_open;
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;

 
 in
 
 fun coinduct_tac ctxt is_open inst taking opt_rule facts =
   let
-    val _ = warn_open ctxt is_open;
+    val _ = warn_open is_open;
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     fun inst_rule r =
       if null inst then `RuleCases.get r