1.1 --- a/src/Pure/Isar/local_syntax.ML	Mon Nov 02 20:45:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_syntax.ML	Mon Nov 02 20:48:08 2009 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    val extern_term: T -> term -> term
     1.5  end;
     1.6  
     1.7 -structure LocalSyntax: LOCAL_SYNTAX =
     1.8 +structure Local_Syntax: LOCAL_SYNTAX =
     1.9  struct
    1.10  
    1.11  (* datatype T *)

     2.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 02 20:45:23 2009 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 02 20:48:08 2009 +0100
     2.3 @@ -166,7 +166,7 @@
     2.4    Ctxt of
     2.5     {mode: mode,                                       (*inner syntax mode*)
     2.6      naming: Name_Space.naming,                        (*local naming conventions*)
     2.7 -    syntax: LocalSyntax.T,                            (*local syntax*)
     2.8 +    syntax: Local_Syntax.T,                           (*local syntax*)
     2.9      consts: Consts.T * Consts.T,                      (*local/global consts*)
    2.10      facts: Facts.T,                                   (*local facts*)
    2.11      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    2.12 @@ -181,7 +181,7 @@
    2.13  (
    2.14    type T = ctxt;
    2.15    fun init thy =
    2.16 -    make_ctxt (mode_default, local_naming, LocalSyntax.init thy,
    2.17 +    make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
    2.18        (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
    2.19  );
    2.20  
    2.21 @@ -230,9 +230,9 @@
    2.22  val full_name = Name_Space.full_name o naming_of;
    2.23  
    2.24  val syntax_of = #syntax o rep_context;
    2.25 -val syn_of = LocalSyntax.syn_of o syntax_of;
    2.26 -val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
    2.27 -val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
    2.28 +val syn_of = Local_Syntax.syn_of o syntax_of;
    2.29 +val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
    2.30 +val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
    2.31  
    2.32  val consts_of = #1 o #consts o rep_context;
    2.33  val const_syntax_name = Consts.syntax_name o consts_of;
    2.34 @@ -247,7 +247,7 @@
    2.35  (* theory transfer *)
    2.36  
    2.37  fun transfer_syntax thy =
    2.38 -  map_syntax (LocalSyntax.rebuild thy) #>
    2.39 +  map_syntax (Local_Syntax.rebuild thy) #>
    2.40    map_consts (fn consts as (local_consts, global_consts) =>
    2.41      let val thy_consts = Sign.consts_of thy in
    2.42        if Consts.eq_consts (thy_consts, global_consts) then consts
    2.43 @@ -710,8 +710,8 @@
    2.44    in
    2.45      t
    2.46      |> Sign.extern_term (Consts.extern_early consts) thy
    2.47 -    |> LocalSyntax.extern_term syntax
    2.48 -    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax)
    2.49 +    |> Local_Syntax.extern_term syntax
    2.50 +    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax)
    2.51          (not (PureThy.old_appl_syntax thy))
    2.52    end;
    2.53  
    2.54 @@ -1029,7 +1029,7 @@
    2.55  
    2.56  fun notation add mode args ctxt =
    2.57    ctxt |> map_syntax
    2.58 -    (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
    2.59 +    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
    2.60  
    2.61  fun target_notation add mode args phi =
    2.62    let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
    2.63 @@ -1083,7 +1083,7 @@
    2.64      val ctxt'' =
    2.65        ctxt'
    2.66        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    2.67 -      |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    2.68 +      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    2.69      val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    2.70        Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
    2.71    in (xs', ctxt'') end;
    2.72 @@ -1316,7 +1316,7 @@
    2.73        val prt_term = Syntax.pretty_term ctxt;
    2.74  
    2.75        (*structures*)
    2.76 -      val structs = LocalSyntax.structs_of (syntax_of ctxt);
    2.77 +      val structs = Local_Syntax.structs_of (syntax_of ctxt);
    2.78        val prt_structs = if null structs then []
    2.79          else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
    2.80            Pretty.commas (map Pretty.str structs))];