1.1 --- a/src/Pure/Isar/local_theory.ML	Mon Nov 02 19:56:06 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Nov 02 20:30:40 2009 +0100
     1.3 @@ -150,9 +150,9 @@
     1.4  fun target_result f lthy =
     1.5    let
     1.6      val (res, ctxt') = target_of lthy
     1.7 -      |> ContextPosition.set_visible false
     1.8 +      |> Context_Position.set_visible false
     1.9        |> f
    1.10 -      ||> ContextPosition.restore_visible lthy;
    1.11 +      ||> Context_Position.restore_visible lthy;
    1.12      val thy' = ProofContext.theory_of ctxt';
    1.13      val lthy' = lthy
    1.14        |> map_target (K ctxt')

     2.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 02 19:56:06 2009 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 02 20:30:40 2009 +0100
     2.3 @@ -932,7 +932,7 @@
     2.4    let
     2.5      val pos = Binding.pos_of b;
     2.6      val name = full_name ctxt b;
     2.7 -    val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
     2.8 +    val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
     2.9  
    2.10      val facts = PureThy.name_thmss false pos name raw_facts;
    2.11      fun app (th, attrs) x =
    2.12 @@ -945,9 +945,9 @@
    2.13  
    2.14  fun put_thms do_props thms ctxt = ctxt
    2.15    |> map_naming (K local_naming)
    2.16 -  |> ContextPosition.set_visible false
    2.17 +  |> Context_Position.set_visible false
    2.18    |> update_thms do_props (apfst Binding.name thms)
    2.19 -  |> ContextPosition.restore_visible ctxt
    2.20 +  |> Context_Position.restore_visible ctxt
    2.21    |> restore_naming ctxt;
    2.22  
    2.23  end;
    2.24 @@ -1085,7 +1085,7 @@
    2.25        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    2.26        |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    2.27      val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    2.28 -      ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
    2.29 +      Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
    2.30    in (xs', ctxt'') end;
    2.31  
    2.32  end;

     3.1 --- a/src/Pure/context_position.ML	Mon Nov 02 19:56:06 2009 +0100
     3.2 +++ b/src/Pure/context_position.ML	Mon Nov 02 20:30:40 2009 +0100
     3.3 @@ -12,7 +12,7 @@
     3.4    val report_visible: Proof.context -> Markup.T -> Position.T -> unit
     3.5  end;
     3.6  
     3.7 -structure ContextPosition: CONTEXT_POSITION =
     3.8 +structure Context_Position: CONTEXT_POSITION =
     3.9  struct
    3.10  
    3.11  structure Data = ProofDataFun