--- a/src/Tools/induct.ML Thu Jan 24 23:51:19 2008 +0100
+++ b/src/Tools/induct.ML Thu Jan 24 23:51:20 2008 +0100
@@ -308,9 +308,9 @@
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 = ();
@@ -336,7 +336,7 @@
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;
@@ -575,7 +575,7 @@
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;
@@ -651,7 +651,7 @@
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;