# HG changeset patch
# User wenzelm
# Date 1201215080 -3600
# Node ID 9ad285dbc7a4e0e4bc74cae30a38b3bd99f24970
# Parent  bcedde463850bde036b1ae58e3cc8f248878f999
replaced ContextPosition by Position.thread_data;

diff -r bcedde463850 -r 9ad285dbc7a4 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Jan 24 23:51:19 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Jan 24 23:51:20 2008 +0100
@@ -119,7 +119,7 @@
     val result = th''
       |> PureThy.name_thm true true ""
       |> Goal.close_result
-      |> fold PureThy.tag_rule (ContextPosition.properties_of ctxt)
+      |> fold PureThy.tag_rule (Position.properties_of (Position.thread_data ()))
       |> PureThy.name_thm true true name;
 
     (*import fixes*)
@@ -206,7 +206,7 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
   let
-    val pos = ContextPosition.properties_of lthy;
+  val pos = Position.properties_of (Position.thread_data ());
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
@@ -234,7 +234,7 @@
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
   let
-    val pos = ContextPosition.properties_of lthy;
+    val pos = Position.properties_of (Position.thread_data ());
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val target_ctxt = LocalTheory.target_of lthy;
 
diff -r bcedde463850 -r 9ad285dbc7a4 src/Tools/induct.ML
--- 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;