# HG changeset patch
# User wenzelm
# Date 1192828873 -7200
# Node ID dfa8001e6264c1467cab0b887f789d928c9fc954
# Parent  ca5708210cb8c1ab018a6454a065e566d55060e4
warn_open: context position;

diff -r ca5708210cb8 -r dfa8001e6264 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Oct 19 23:21:11 2007 +0200
+++ b/src/Tools/induct.ML	Fri Oct 19 23:21:13 2007 +0200
@@ -308,8 +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 true = legacy_feature "open rule cases in proof method"
-  | warn_open false = ();
+fun warn_open ctxt true =
+      legacy_feature ("open rule cases in proof method" ^ ContextPosition.str_of ctxt)
+  | warn_open _ false = ();
 
 
 
@@ -335,7 +336,7 @@
 
 fun cases_tac ctxt is_open insts opt_rule facts =
   let
-    val _ = warn_open is_open;
+    val _ = warn_open ctxt is_open;
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
@@ -574,7 +575,7 @@
 
 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
   let
-    val _ = warn_open is_open;
+    val _ = warn_open ctxt is_open;
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
@@ -650,7 +651,7 @@
 
 fun coinduct_tac ctxt is_open inst taking opt_rule facts =
   let
-    val _ = warn_open is_open;
+    val _ = warn_open ctxt is_open;
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;