# HG changeset patch
# User wenzelm
# Date 1257190240 -3600
# Node ID 12d79ece3f7eb3b0f3f7df59fab1ee8733bdd1f1
# Parent  7d2c6e7f91bd07cbacdc3ddcd6e2424c78f75be9
modernized structure Context_Position;

diff -r 7d2c6e7f91bd -r 12d79ece3f7e src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Nov 02 19:56:06 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Mon Nov 02 20:30:40 2009 +0100
@@ -150,9 +150,9 @@
 fun target_result f lthy =
   let
     val (res, ctxt') = target_of lthy
-      |> ContextPosition.set_visible false
+      |> Context_Position.set_visible false
       |> f
-      ||> ContextPosition.restore_visible lthy;
+      ||> Context_Position.restore_visible lthy;
     val thy' = ProofContext.theory_of ctxt';
     val lthy' = lthy
       |> map_target (K ctxt')
diff -r 7d2c6e7f91bd -r 12d79ece3f7e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Nov 02 19:56:06 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 02 20:30:40 2009 +0100
@@ -932,7 +932,7 @@
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
-    val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
+    val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
 
     val facts = PureThy.name_thmss false pos name raw_facts;
     fun app (th, attrs) x =
@@ -945,9 +945,9 @@
 
 fun put_thms do_props thms ctxt = ctxt
   |> map_naming (K local_naming)
-  |> ContextPosition.set_visible false
+  |> Context_Position.set_visible false
   |> update_thms do_props (apfst Binding.name thms)
-  |> ContextPosition.restore_visible ctxt
+  |> Context_Position.restore_visible ctxt
   |> restore_naming ctxt;
 
 end;
@@ -1085,7 +1085,7 @@
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
       |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
     val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
-      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+      Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
 end;
diff -r 7d2c6e7f91bd -r 12d79ece3f7e src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Mon Nov 02 19:56:06 2009 +0100
+++ b/src/Pure/context_position.ML	Mon Nov 02 20:30:40 2009 +0100
@@ -12,7 +12,7 @@
   val report_visible: Proof.context -> Markup.T -> Position.T -> unit
 end;
 
-structure ContextPosition: CONTEXT_POSITION =
+structure Context_Position: CONTEXT_POSITION =
 struct
 
 structure Data = ProofDataFun