src/Pure/Isar/proof_context.ML
changeset 33387 acea2f336721
parent 33386 ff29d1549aca
child 33519 e31a85f92ce9
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 02 20:45:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 02 20:48:08 2009 +0100
     1.3 @@ -166,7 +166,7 @@
     1.4    Ctxt of
     1.5     {mode: mode,                                       (*inner syntax mode*)
     1.6      naming: Name_Space.naming,                        (*local naming conventions*)
     1.7 -    syntax: LocalSyntax.T,                            (*local syntax*)
     1.8 +    syntax: Local_Syntax.T,                           (*local syntax*)
     1.9      consts: Consts.T * Consts.T,                      (*local/global consts*)
    1.10      facts: Facts.T,                                   (*local facts*)
    1.11      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    1.12 @@ -181,7 +181,7 @@
    1.13  (
    1.14    type T = ctxt;
    1.15    fun init thy =
    1.16 -    make_ctxt (mode_default, local_naming, LocalSyntax.init thy,
    1.17 +    make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
    1.18        (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
    1.19  );
    1.20  
    1.21 @@ -230,9 +230,9 @@
    1.22  val full_name = Name_Space.full_name o naming_of;
    1.23  
    1.24  val syntax_of = #syntax o rep_context;
    1.25 -val syn_of = LocalSyntax.syn_of o syntax_of;
    1.26 -val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
    1.27 -val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
    1.28 +val syn_of = Local_Syntax.syn_of o syntax_of;
    1.29 +val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
    1.30 +val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
    1.31  
    1.32  val consts_of = #1 o #consts o rep_context;
    1.33  val const_syntax_name = Consts.syntax_name o consts_of;
    1.34 @@ -247,7 +247,7 @@
    1.35  (* theory transfer *)
    1.36  
    1.37  fun transfer_syntax thy =
    1.38 -  map_syntax (LocalSyntax.rebuild thy) #>
    1.39 +  map_syntax (Local_Syntax.rebuild thy) #>
    1.40    map_consts (fn consts as (local_consts, global_consts) =>
    1.41      let val thy_consts = Sign.consts_of thy in
    1.42        if Consts.eq_consts (thy_consts, global_consts) then consts
    1.43 @@ -710,8 +710,8 @@
    1.44    in
    1.45      t
    1.46      |> Sign.extern_term (Consts.extern_early consts) thy
    1.47 -    |> LocalSyntax.extern_term syntax
    1.48 -    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax)
    1.49 +    |> Local_Syntax.extern_term syntax
    1.50 +    |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (Local_Syntax.syn_of syntax)
    1.51          (not (PureThy.old_appl_syntax thy))
    1.52    end;
    1.53  
    1.54 @@ -1029,7 +1029,7 @@
    1.55  
    1.56  fun notation add mode args ctxt =
    1.57    ctxt |> map_syntax
    1.58 -    (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
    1.59 +    (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
    1.60  
    1.61  fun target_notation add mode args phi =
    1.62    let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
    1.63 @@ -1083,7 +1083,7 @@
    1.64      val ctxt'' =
    1.65        ctxt'
    1.66        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    1.67 -      |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    1.68 +      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map prep_mixfix);
    1.69      val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    1.70        Context_Position.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
    1.71    in (xs', ctxt'') end;
    1.72 @@ -1316,7 +1316,7 @@
    1.73        val prt_term = Syntax.pretty_term ctxt;
    1.74  
    1.75        (*structures*)
    1.76 -      val structs = LocalSyntax.structs_of (syntax_of ctxt);
    1.77 +      val structs = Local_Syntax.structs_of (syntax_of ctxt);
    1.78        val prt_structs = if null structs then []
    1.79          else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
    1.80            Pretty.commas (map Pretty.str structs))];