renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
authorwenzelm
Sat Oct 24 19:47:37 2009 +0200 (2009-10-24)
changeset 33095bbd52d2f8696
parent 33094 ef0d77b1e687
child 33096 db3c18fd9708
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
src/HOL/Tools/inductive.ML
src/HOL/Tools/record.ML
src/HOL/Tools/res_atp.ML
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_theorems.ML
src/Pure/consts.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/facts.ML
src/Pure/name.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Sat Oct 24 19:24:50 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Oct 24 19:47:37 2009 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4      val (tab, monos) = get_inductives ctxt;
     1.5      val space = Consts.space_of (ProofContext.consts_of ctxt);
     1.6    in
     1.7 -    [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
     1.8 +    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
     1.9       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
    1.10      |> Pretty.chunks |> Pretty.writeln
    1.11    end;
     2.1 --- a/src/HOL/Tools/record.ML	Sat Oct 24 19:24:50 2009 +0200
     2.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 24 19:47:37 2009 +0200
     2.3 @@ -1810,7 +1810,7 @@
     2.4  
     2.5  fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
     2.6    let
     2.7 -    val external_names = NameSpace.external_names (Sign.naming_of thy);
     2.8 +    val external_names = Name_Space.external_names (Sign.naming_of thy);
     2.9  
    2.10      val alphas = map fst args;
    2.11      val name = Sign.full_bname thy bname;
     3.1 --- a/src/HOL/Tools/res_atp.ML	Sat Oct 24 19:24:50 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Sat Oct 24 19:47:37 2009 +0200
     3.3 @@ -355,7 +355,7 @@
     3.4      if run_blacklist_filter andalso is_package_def name then I
     3.5      else
     3.6        let val xname = Facts.extern facts name in
     3.7 -        if NameSpace.is_hidden xname then I
     3.8 +        if Name_Space.is_hidden xname then I
     3.9          else cons (xname, filter_out ResAxioms.bad_for_atp ths)
    3.10        end) facts [];
    3.11  
     4.1 --- a/src/Pure/General/name_space.ML	Sat Oct 24 19:24:50 2009 +0200
     4.2 +++ b/src/Pure/General/name_space.ML	Sat Oct 24 19:47:37 2009 +0200
     4.3 @@ -46,7 +46,7 @@
     4.4    val extern_table: 'a table -> (xstring * 'a) list
     4.5  end;
     4.6  
     4.7 -structure NameSpace: NAME_SPACE =
     4.8 +structure Name_Space: NAME_SPACE =
     4.9  struct
    4.10  
    4.11  
    4.12 @@ -79,13 +79,13 @@
    4.13  (* datatype T *)
    4.14  
    4.15  datatype T =
    4.16 -  NameSpace of
    4.17 +  Name_Space of
    4.18      (string list * string list) Symtab.table *   (*internals, hidden internals*)
    4.19      entry Symtab.table;
    4.20  
    4.21 -val empty = NameSpace (Symtab.empty, Symtab.empty);
    4.22 +val empty = Name_Space (Symtab.empty, Symtab.empty);
    4.23  
    4.24 -fun lookup (NameSpace (tab, _)) xname =
    4.25 +fun lookup (Name_Space (tab, _)) xname =
    4.26    (case Symtab.lookup tab xname of
    4.27      NONE => (xname, true)
    4.28    | SOME ([], []) => (xname, true)
    4.29 @@ -93,12 +93,12 @@
    4.30    | SOME (name :: _, _) => (name, false)
    4.31    | SOME ([], name' :: _) => (hidden name', true));
    4.32  
    4.33 -fun get_accesses (NameSpace (_, entries)) name =
    4.34 +fun get_accesses (Name_Space (_, entries)) name =
    4.35    (case Symtab.lookup entries name of
    4.36      NONE => [name]
    4.37    | SOME {externals, ...} => externals);
    4.38  
    4.39 -fun valid_accesses (NameSpace (tab, _)) name =
    4.40 +fun valid_accesses (Name_Space (tab, _)) name =
    4.41    Symtab.fold (fn (xname, (names, _)) =>
    4.42      if not (null names) andalso hd names = name then cons xname else I) tab [];
    4.43  
    4.44 @@ -136,8 +136,8 @@
    4.45  
    4.46  local
    4.47  
    4.48 -fun map_space f xname (NameSpace (tab, entries)) =
    4.49 -  NameSpace (Symtab.map_default (xname, ([], [])) f tab, entries);
    4.50 +fun map_space f xname (Name_Space (tab, entries)) =
    4.51 +  Name_Space (Symtab.map_default (xname, ([], [])) f tab, entries);
    4.52  
    4.53  in
    4.54  
    4.55 @@ -168,7 +168,7 @@
    4.56  
    4.57  (* merge *)
    4.58  
    4.59 -fun merge (NameSpace (tab1, entries1), NameSpace (tab2, entries2)) =
    4.60 +fun merge (Name_Space (tab1, entries1), Name_Space (tab2, entries2)) =
    4.61    let
    4.62      val tab' = (tab1, tab2) |> Symtab.join
    4.63        (K (fn ((names1, names1'), (names2, names2')) =>
    4.64 @@ -182,7 +182,7 @@
    4.65            error ("Duplicate declaration " ^
    4.66              quote (str_of_entry true (name, entry1)) ^ " vs. " ^
    4.67              quote (str_of_entry true (name, entry2))));
    4.68 -  in NameSpace (tab', entries') end;
    4.69 +  in Name_Space (tab', entries') end;
    4.70  
    4.71  
    4.72  
    4.73 @@ -245,13 +245,13 @@
    4.74  
    4.75  (* declaration *)
    4.76  
    4.77 -fun new_entry strict entry (NameSpace (tab, entries)) =
    4.78 +fun new_entry strict entry (Name_Space (tab, entries)) =
    4.79    let
    4.80      val entries' =
    4.81        (if strict then Symtab.update_new else Symtab.update) entry entries
    4.82          handle Symtab.DUP _ =>
    4.83            error ("Duplicate declaration " ^ quote (str_of_entry true entry));
    4.84 -  in NameSpace (tab, entries') end;
    4.85 +  in Name_Space (tab, entries') end;
    4.86  
    4.87  fun declare strict naming binding space =
    4.88    let
    4.89 @@ -294,6 +294,6 @@
    4.90  
    4.91  end;
    4.92  
    4.93 -structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
    4.94 +structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
    4.95  open Basic_Name_Space;
    4.96  
     5.1 --- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:24:50 2009 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 19:47:37 2009 +0200
     5.3 @@ -67,11 +67,11 @@
     5.4  
     5.5  structure Attributes = TheoryDataFun
     5.6  (
     5.7 -  type T = ((src -> attribute) * string) NameSpace.table;
     5.8 -  val empty = NameSpace.empty_table;
     5.9 +  type T = ((src -> attribute) * string) Name_Space.table;
    5.10 +  val empty = Name_Space.empty_table;
    5.11    val copy = I;
    5.12    val extend = I;
    5.13 -  fun merge _ tables : T = NameSpace.merge_tables tables;
    5.14 +  fun merge _ tables : T = Name_Space.merge_tables tables;
    5.15  );
    5.16  
    5.17  fun print_attributes thy =
    5.18 @@ -80,20 +80,20 @@
    5.19      fun prt_attr (name, (_, comment)) = Pretty.block
    5.20        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    5.21    in
    5.22 -    [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
    5.23 +    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
    5.24      |> Pretty.chunks |> Pretty.writeln
    5.25    end;
    5.26  
    5.27  fun add_attribute name att comment thy = thy
    5.28 -  |> Attributes.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (att, comment)));
    5.29 +  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
    5.30  
    5.31  
    5.32  (* name space *)
    5.33  
    5.34 -val intern = NameSpace.intern o #1 o Attributes.get;
    5.35 +val intern = Name_Space.intern o #1 o Attributes.get;
    5.36  val intern_src = Args.map_name o intern;
    5.37  
    5.38 -val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
    5.39 +val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
    5.40  
    5.41  
    5.42  (* pretty printing *)
    5.43 @@ -338,7 +338,7 @@
    5.44          Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
    5.45            Pretty.str (Config.print_value value)]
    5.46        end;
    5.47 -    val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
    5.48 +    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
    5.49    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    5.50  
    5.51  
     6.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Oct 24 19:24:50 2009 +0200
     6.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Oct 24 19:47:37 2009 +0200
     6.3 @@ -400,7 +400,7 @@
     6.4      val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
     6.5      val {classes, ...} = Sorts.rep_algebra algebra;
     6.6      fun entry (c, (i, (_, cs))) =
     6.7 -      (i, {name = NameSpace.extern space c, ID = c, parents = cs,
     6.8 +      (i, {name = Name_Space.extern space c, ID = c, parents = cs,
     6.9              dir = "", unfold = true, path = ""});
    6.10      val gr =
    6.11        Graph.fold (cons o entry) classes []
     7.1 --- a/src/Pure/Isar/local_theory.ML	Sat Oct 24 19:24:50 2009 +0200
     7.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Oct 24 19:47:37 2009 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     7.5    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     7.6    val checkpoint: local_theory -> local_theory
     7.7 -  val full_naming: local_theory -> NameSpace.naming
     7.8 +  val full_naming: local_theory -> Name_Space.naming
     7.9    val full_name: local_theory -> binding -> string
    7.10    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    7.11    val theory: (theory -> theory) -> local_theory -> local_theory
    7.12 @@ -139,9 +139,9 @@
    7.13  
    7.14  fun full_naming lthy =
    7.15    Sign.naming_of (ProofContext.theory_of lthy)
    7.16 -  |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
    7.17 +  |> Name_Space.mandatory_path (#theory_prefix (get_lthy lthy));
    7.18  
    7.19 -fun full_name naming = NameSpace.full_name (full_naming naming);
    7.20 +fun full_name naming = Name_Space.full_name (full_naming naming);
    7.21  
    7.22  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    7.23    |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
     8.1 --- a/src/Pure/Isar/locale.ML	Sat Oct 24 19:24:50 2009 +0200
     8.2 +++ b/src/Pure/Isar/locale.ML	Sat Oct 24 19:47:37 2009 +0200
     8.3 @@ -124,15 +124,15 @@
     8.4  
     8.5  structure Locales = TheoryDataFun
     8.6  (
     8.7 -  type T = locale NameSpace.table;
     8.8 -  val empty = NameSpace.empty_table;
     8.9 +  type T = locale Name_Space.table;
    8.10 +  val empty = Name_Space.empty_table;
    8.11    val copy = I;
    8.12    val extend = I;
    8.13 -  fun merge _ = NameSpace.join_tables (K merge_locale);
    8.14 +  fun merge _ = Name_Space.join_tables (K merge_locale);
    8.15  );
    8.16  
    8.17 -val intern = NameSpace.intern o #1 o Locales.get;
    8.18 -val extern = NameSpace.extern o #1 o Locales.get;
    8.19 +val intern = Name_Space.intern o #1 o Locales.get;
    8.20 +val extern = Name_Space.extern o #1 o Locales.get;
    8.21  
    8.22  val get_locale = Symtab.lookup o #2 o Locales.get;
    8.23  val defined = Symtab.defined o #2 o Locales.get;
    8.24 @@ -143,7 +143,7 @@
    8.25    | NONE => error ("Unknown locale " ^ quote name));
    8.26  
    8.27  fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
    8.28 -  thy |> Locales.map (NameSpace.define true (Sign.naming_of thy)
    8.29 +  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
    8.30      (binding,
    8.31        mk_locale ((parameters, spec, intros, axioms),
    8.32          ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
    8.33 @@ -153,7 +153,7 @@
    8.34    Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
    8.35  
    8.36  fun print_locales thy =
    8.37 -  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (Locales.get thy)))
    8.38 +  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
    8.39    |> Pretty.writeln;
    8.40  
    8.41  
     9.1 --- a/src/Pure/Isar/method.ML	Sat Oct 24 19:24:50 2009 +0200
     9.2 +++ b/src/Pure/Isar/method.ML	Sat Oct 24 19:47:37 2009 +0200
     9.3 @@ -322,11 +322,11 @@
     9.4  
     9.5  structure Methods = TheoryDataFun
     9.6  (
     9.7 -  type T = ((src -> Proof.context -> method) * string) NameSpace.table;
     9.8 -  val empty = NameSpace.empty_table;
     9.9 +  type T = ((src -> Proof.context -> method) * string) Name_Space.table;
    9.10 +  val empty = Name_Space.empty_table;
    9.11    val copy = I;
    9.12    val extend = I;
    9.13 -  fun merge _ tables : T = NameSpace.merge_tables tables;
    9.14 +  fun merge _ tables : T = Name_Space.merge_tables tables;
    9.15  );
    9.16  
    9.17  fun print_methods thy =
    9.18 @@ -335,17 +335,17 @@
    9.19      fun prt_meth (name, (_, comment)) = Pretty.block
    9.20        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
    9.21    in
    9.22 -    [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
    9.23 +    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))]
    9.24      |> Pretty.chunks |> Pretty.writeln
    9.25    end;
    9.26  
    9.27  fun add_method name meth comment thy = thy
    9.28 -  |> Methods.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (meth, comment)));
    9.29 +  |> Methods.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (meth, comment)));
    9.30  
    9.31  
    9.32  (* get methods *)
    9.33  
    9.34 -val intern = NameSpace.intern o #1 o Methods.get;
    9.35 +val intern = Name_Space.intern o #1 o Methods.get;
    9.36  val defined = Symtab.defined o #2 o Methods.get;
    9.37  
    9.38  fun method_i thy =
    9.39 @@ -359,7 +359,7 @@
    9.40        end;
    9.41    in meth end;
    9.42  
    9.43 -fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
    9.44 +fun method thy = method_i thy o Args.map_name (Name_Space.intern (#1 (Methods.get thy)));
    9.45  
    9.46  
    9.47  (* method setup *)
    10.1 --- a/src/Pure/Isar/proof_context.ML	Sat Oct 24 19:24:50 2009 +0200
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Oct 24 19:47:37 2009 +0200
    10.3 @@ -21,7 +21,7 @@
    10.4    val restore_mode: Proof.context -> Proof.context -> Proof.context
    10.5    val abbrev_mode: Proof.context -> bool
    10.6    val set_stmt: bool -> Proof.context -> Proof.context
    10.7 -  val naming_of: Proof.context -> NameSpace.naming
    10.8 +  val naming_of: Proof.context -> Name_Space.naming
    10.9    val full_name: Proof.context -> binding -> string
   10.10    val consts_of: Proof.context -> Consts.T
   10.11    val const_syntax_name: Proof.context -> string -> string
   10.12 @@ -170,7 +170,7 @@
   10.13  datatype ctxt =
   10.14    Ctxt of
   10.15     {mode: mode,                                       (*inner syntax mode*)
   10.16 -    naming: NameSpace.naming,                         (*local naming conventions*)
   10.17 +    naming: Name_Space.naming,                        (*local naming conventions*)
   10.18      syntax: LocalSyntax.T,                            (*local syntax*)
   10.19      consts: Consts.T * Consts.T,                      (*local/global consts*)
   10.20      facts: Facts.T,                                   (*local facts*)
   10.21 @@ -180,7 +180,7 @@
   10.22    Ctxt {mode = mode, naming = naming, syntax = syntax,
   10.23      consts = consts, facts = facts, cases = cases};
   10.24  
   10.25 -val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
   10.26 +val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
   10.27  
   10.28  structure ContextData = ProofDataFun
   10.29  (
   10.30 @@ -231,7 +231,7 @@
   10.31    map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
   10.32  
   10.33  val naming_of = #naming o rep_context;
   10.34 -val full_name = NameSpace.full_name o naming_of;
   10.35 +val full_name = Name_Space.full_name o naming_of;
   10.36  
   10.37  val syntax_of = #syntax o rep_context;
   10.38  val syn_of = LocalSyntax.syn_of o syntax_of;
   10.39 @@ -924,10 +924,10 @@
   10.40  
   10.41  (* name space operations *)
   10.42  
   10.43 -val add_path        = map_naming o NameSpace.add_path;
   10.44 -val mandatory_path  = map_naming o NameSpace.mandatory_path;
   10.45 -val restore_naming  = map_naming o K o naming_of;
   10.46 -val reset_naming    = map_naming (K local_naming);
   10.47 +val add_path = map_naming o Name_Space.add_path;
   10.48 +val mandatory_path = map_naming o Name_Space.mandatory_path;
   10.49 +val restore_naming = map_naming o K o naming_of;
   10.50 +val reset_naming = map_naming (K local_naming);
   10.51  
   10.52  
   10.53  (* facts *)
   10.54 @@ -1230,7 +1230,7 @@
   10.55        | add_abbr (c, (T, SOME t)) =
   10.56            if not show_globals andalso Symtab.defined globals c then I
   10.57            else cons (c, Logic.mk_equals (Const (c, T), t));
   10.58 -    val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
   10.59 +    val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
   10.60    in
   10.61      if null abbrevs andalso not (! verbose) then []
   10.62      else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
    11.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:24:50 2009 +0200
    11.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:47:37 2009 +0200
    11.3 @@ -420,9 +420,9 @@
    11.4    ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
    11.5    ("show_structs", setmp_CRITICAL show_structs o boolean),
    11.6    ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
    11.7 -  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
    11.8 -  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
    11.9 -  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
   11.10 +  ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
   11.11 +  ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
   11.12 +  ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
   11.13    ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   11.14    ("display", setmp_CRITICAL display o boolean),
   11.15    ("break", setmp_CRITICAL break o boolean),
    12.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Oct 24 19:24:50 2009 +0200
    12.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Oct 24 19:47:37 2009 +0200
    12.3 @@ -326,7 +326,7 @@
    12.4  local
    12.5  
    12.6  val index_ord = option_ord (K EQUAL);
    12.7 -val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
    12.8 +val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
    12.9  val qual_ord = int_ord o pairself (length o Long_Name.explode);
   12.10  val txt_ord = int_ord o pairself size;
   12.11  
   12.12 @@ -355,7 +355,8 @@
   12.13      val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
   12.14  
   12.15      val shorten =
   12.16 -      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
   12.17 +      Name_Space.extern_flags
   12.18 +        {long_names = false, short_names = false, unique_names = false} space;
   12.19  
   12.20      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
   12.21            nicer_name (shorten x, i) (shorten y, j)
    13.1 --- a/src/Pure/consts.ML	Sat Oct 24 19:24:50 2009 +0200
    13.2 +++ b/src/Pure/consts.ML	Sat Oct 24 19:47:37 2009 +0200
    13.3 @@ -11,15 +11,15 @@
    13.4    val eq_consts: T * T -> bool
    13.5    val retrieve_abbrevs: T -> string list -> term -> (term * term) list
    13.6    val dest: T ->
    13.7 -   {constants: (typ * term option) NameSpace.table,
    13.8 -    constraints: typ NameSpace.table}
    13.9 +   {constants: (typ * term option) Name_Space.table,
   13.10 +    constraints: typ Name_Space.table}
   13.11    val the_type: T -> string -> typ                             (*exception TYPE*)
   13.12    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   13.13    val type_scheme: T -> string -> typ                          (*exception TYPE*)
   13.14    val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
   13.15    val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   13.16    val the_constraint: T -> string -> typ                       (*exception TYPE*)
   13.17 -  val space_of: T -> NameSpace.T
   13.18 +  val space_of: T -> Name_Space.T
   13.19    val intern: T -> xstring -> string
   13.20    val extern: T -> string -> xstring
   13.21    val extern_early: T -> string -> xstring
   13.22 @@ -29,9 +29,9 @@
   13.23    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   13.24    val typargs: T -> string * typ -> typ list
   13.25    val instance: T -> string * typ list -> typ
   13.26 -  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
   13.27 +  val declare: bool -> Name_Space.naming -> Properties.T -> (binding * typ) -> T -> T
   13.28    val constrain: string * typ option -> T -> T
   13.29 -  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
   13.30 +  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
   13.31      binding * term -> T -> (term * term) * T
   13.32    val revert_abbrev: string -> string -> T -> T
   13.33    val hide: bool -> string -> T -> T
   13.34 @@ -50,7 +50,7 @@
   13.35  type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
   13.36  
   13.37  datatype T = Consts of
   13.38 - {decls: (decl * abbrev option) NameSpace.table,
   13.39 + {decls: (decl * abbrev option) Name_Space.table,
   13.40    constraints: typ Symtab.table,
   13.41    rev_abbrevs: (term * term) Item_Net.T Symtab.table};
   13.42  
   13.43 @@ -123,8 +123,8 @@
   13.44  
   13.45  fun space_of (Consts {decls = (space, _), ...}) = space;
   13.46  
   13.47 -val intern = NameSpace.intern o space_of;
   13.48 -val extern = NameSpace.extern o space_of;
   13.49 +val intern = Name_Space.intern o space_of;
   13.50 +val extern = Name_Space.extern o space_of;
   13.51  
   13.52  fun extern_early consts c =
   13.53    (case try (the_const consts) c of
   13.54 @@ -224,7 +224,7 @@
   13.55  (* name space *)
   13.56  
   13.57  fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
   13.58 -  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs));
   13.59 +  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
   13.60  
   13.61  
   13.62  (* declarations *)
   13.63 @@ -234,7 +234,7 @@
   13.64      let
   13.65        val tags' = tags |> Position.default_properties (Position.thread_data ());
   13.66        val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
   13.67 -      val (_, decls') = decls |> NameSpace.define true naming (b, (decl, NONE));
   13.68 +      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
   13.69      in (decls', constraints, rev_abbrevs) end);
   13.70  
   13.71  
   13.72 @@ -280,7 +280,7 @@
   13.73        |> Term.close_schematic_term;
   13.74      val normal_rhs = expand_term rhs;
   13.75      val T = Term.fastype_of rhs;
   13.76 -    val lhs = Const (NameSpace.full_name naming b, T);
   13.77 +    val lhs = Const (Name_Space.full_name naming b, T);
   13.78    in
   13.79      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
   13.80        let
   13.81 @@ -288,7 +288,7 @@
   13.82          val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
   13.83          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
   13.84          val (_, decls') = decls
   13.85 -          |> NameSpace.define true naming (b, (decl, SOME abbr));
   13.86 +          |> Name_Space.define true naming (b, (decl, SOME abbr));
   13.87          val rev_abbrevs' = rev_abbrevs
   13.88            |> insert_abbrevs mode (rev_abbrev lhs rhs);
   13.89        in (decls', constraints, rev_abbrevs') end)
   13.90 @@ -307,13 +307,13 @@
   13.91  
   13.92  (* empty and merge *)
   13.93  
   13.94 -val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
   13.95 +val empty = make_consts (Name_Space.empty_table, Symtab.empty, Symtab.empty);
   13.96  
   13.97  fun merge
   13.98     (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
   13.99      Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
  13.100    let
  13.101 -    val decls' = NameSpace.merge_tables (decls1, decls2);
  13.102 +    val decls' = Name_Space.merge_tables (decls1, decls2);
  13.103      val constraints' = Symtab.join (K fst) (constraints1, constraints2);
  13.104      val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
  13.105    in make_consts (decls', constraints', rev_abbrevs') end;
    14.1 --- a/src/Pure/display.ML	Sat Oct 24 19:24:50 2009 +0200
    14.2 +++ b/src/Pure/display.ML	Sat Oct 24 19:47:37 2009 +0200
    14.3 @@ -179,25 +179,25 @@
    14.4      val {restricts, reducts} = Defs.dest defs;
    14.5      val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
    14.6      val {constants, constraints} = Consts.dest consts;
    14.7 -    val extern_const = NameSpace.extern (#1 constants);
    14.8 +    val extern_const = Name_Space.extern (#1 constants);
    14.9      val {classes, default, types, ...} = Type.rep_tsig tsig;
   14.10      val (class_space, class_algebra) = classes;
   14.11      val {classes, arities} = Sorts.rep_algebra class_algebra;
   14.12  
   14.13 -    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
   14.14 -    val tdecls = NameSpace.dest_table types;
   14.15 -    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
   14.16 +    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
   14.17 +    val tdecls = Name_Space.dest_table types;
   14.18 +    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
   14.19  
   14.20      fun prune_const c = not verbose andalso
   14.21        member (op =) (Consts.the_tags consts c) Markup.property_internal;
   14.22 -    val cnsts = NameSpace.extern_table (#1 constants,
   14.23 +    val cnsts = Name_Space.extern_table (#1 constants,
   14.24        Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
   14.25  
   14.26      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   14.27      val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   14.28 -    val cnstrs = NameSpace.extern_table constraints;
   14.29 +    val cnstrs = Name_Space.extern_table constraints;
   14.30  
   14.31 -    val axms = NameSpace.extern_table axioms;
   14.32 +    val axms = Name_Space.extern_table axioms;
   14.33  
   14.34      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   14.35        |> map (fn (lhs, rhs) =>
    15.1 --- a/src/Pure/drule.ML	Sat Oct 24 19:24:50 2009 +0200
    15.2 +++ b/src/Pure/drule.ML	Sat Oct 24 19:47:37 2009 +0200
    15.3 @@ -452,7 +452,7 @@
    15.4  
    15.5  val read_prop = certify o SimpleSyntax.read_prop;
    15.6  
    15.7 -fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
    15.8 +fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
    15.9  
   15.10  fun store_thm name th =
   15.11    Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));
    16.1 --- a/src/Pure/facts.ML	Sat Oct 24 19:24:50 2009 +0200
    16.2 +++ b/src/Pure/facts.ML	Sat Oct 24 19:47:37 2009 +0200
    16.3 @@ -20,7 +20,7 @@
    16.4    val selections: string * thm list -> (ref * thm) list
    16.5    type T
    16.6    val empty: T
    16.7 -  val space_of: T -> NameSpace.T
    16.8 +  val space_of: T -> Name_Space.T
    16.9    val intern: T -> xstring -> string
   16.10    val extern: T -> string -> xstring
   16.11    val lookup: Context.generic -> T -> string -> (bool * thm list) option
   16.12 @@ -31,9 +31,9 @@
   16.13    val props: T -> thm list
   16.14    val could_unify: T -> term -> thm list
   16.15    val merge: T * T -> T
   16.16 -  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
   16.17 -  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
   16.18 -  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   16.19 +  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
   16.20 +  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
   16.21 +  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   16.22    val del: string -> T -> T
   16.23    val hide: bool -> string -> T -> T
   16.24  end;
   16.25 @@ -122,11 +122,11 @@
   16.26  datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
   16.27  
   16.28  datatype T = Facts of
   16.29 - {facts: fact NameSpace.table,
   16.30 + {facts: fact Name_Space.table,
   16.31    props: thm Net.net};
   16.32  
   16.33  fun make_facts facts props = Facts {facts = facts, props = props};
   16.34 -val empty = make_facts NameSpace.empty_table Net.empty;
   16.35 +val empty = make_facts Name_Space.empty_table Net.empty;
   16.36  
   16.37  
   16.38  (* named facts *)
   16.39 @@ -136,8 +136,8 @@
   16.40  val space_of = #1 o facts_of;
   16.41  val table_of = #2 o facts_of;
   16.42  
   16.43 -val intern = NameSpace.intern o space_of;
   16.44 -val extern = NameSpace.extern o space_of;
   16.45 +val intern = Name_Space.intern o space_of;
   16.46 +val extern = Name_Space.extern o space_of;
   16.47  
   16.48  val defined = Symtab.defined o table_of;
   16.49  
   16.50 @@ -177,7 +177,7 @@
   16.51  
   16.52  fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   16.53    let
   16.54 -    val facts' = NameSpace.merge_tables (facts1, facts2);
   16.55 +    val facts' = Name_Space.merge_tables (facts1, facts2);
   16.56      val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   16.57    in make_facts facts' props' end;
   16.58  
   16.59 @@ -190,7 +190,7 @@
   16.60    let
   16.61      val (name, facts') =
   16.62        if Binding.is_empty b then ("", facts)
   16.63 -      else NameSpace.define strict naming (b, Static ths) facts;
   16.64 +      else Name_Space.define strict naming (b, Static ths) facts;
   16.65      val props' =
   16.66        if do_props
   16.67        then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   16.68 @@ -208,7 +208,7 @@
   16.69  (* add dynamic entries *)
   16.70  
   16.71  fun add_dynamic naming (b, f) (Facts {facts, props}) =
   16.72 -  let val (name, facts') = NameSpace.define true naming (b, Dynamic f) facts;
   16.73 +  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
   16.74    in (name, make_facts facts' props) end;
   16.75  
   16.76  
   16.77 @@ -216,11 +216,11 @@
   16.78  
   16.79  fun del name (Facts {facts = (space, tab), props}) =
   16.80    let
   16.81 -    val space' = NameSpace.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
   16.82 +    val space' = Name_Space.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
   16.83      val tab' = Symtab.delete_safe name tab;
   16.84    in make_facts (space', tab') props end;
   16.85  
   16.86  fun hide fully name (Facts {facts = (space, tab), props}) =
   16.87 -  make_facts (NameSpace.hide fully name space, tab) props;
   16.88 +  make_facts (Name_Space.hide fully name space, tab) props;
   16.89  
   16.90  end;
    17.1 --- a/src/Pure/name.ML	Sat Oct 24 19:24:50 2009 +0200
    17.2 +++ b/src/Pure/name.ML	Sat Oct 24 19:47:37 2009 +0200
    17.3 @@ -45,7 +45,7 @@
    17.4  
    17.5  (* checked binding *)
    17.6  
    17.7 -val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
    17.8 +val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
    17.9  
   17.10  
   17.11  (* encoded bounds *)
    18.1 --- a/src/Pure/pure_thy.ML	Sat Oct 24 19:24:50 2009 +0200
    18.2 +++ b/src/Pure/pure_thy.ML	Sat Oct 24 19:47:37 2009 +0200
    18.3 @@ -146,7 +146,7 @@
    18.4    else
    18.5      let
    18.6        val naming = Sign.naming_of thy;
    18.7 -      val name = NameSpace.full_name naming b;
    18.8 +      val name = Name_Space.full_name naming b;
    18.9        val (thy', thms') =
   18.10          register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
   18.11        val thms'' = map (Thm.transfer thy') thms';
    19.1 --- a/src/Pure/sign.ML	Sat Oct 24 19:24:50 2009 +0200
    19.2 +++ b/src/Pure/sign.ML	Sat Oct 24 19:47:37 2009 +0200
    19.3 @@ -8,11 +8,11 @@
    19.4  signature SIGN =
    19.5  sig
    19.6    val rep_sg: theory ->
    19.7 -   {naming: NameSpace.naming,
    19.8 +   {naming: Name_Space.naming,
    19.9      syn: Syntax.syntax,
   19.10      tsig: Type.tsig,
   19.11      consts: Consts.T}
   19.12 -  val naming_of: theory -> NameSpace.naming
   19.13 +  val naming_of: theory -> Name_Space.naming
   19.14    val full_name: theory -> binding -> string
   19.15    val full_name_path: theory -> string -> binding -> string
   19.16    val full_bname: theory -> bstring -> string
   19.17 @@ -44,9 +44,9 @@
   19.18    val const_typargs: theory -> string * typ -> typ list
   19.19    val const_instance: theory -> string * typ list -> typ
   19.20    val mk_const: theory -> string * typ list -> term
   19.21 -  val class_space: theory -> NameSpace.T
   19.22 -  val type_space: theory -> NameSpace.T
   19.23 -  val const_space: theory -> NameSpace.T
   19.24 +  val class_space: theory -> Name_Space.T
   19.25 +  val type_space: theory -> Name_Space.T
   19.26 +  val const_space: theory -> Name_Space.T
   19.27    val intern_class: theory -> xstring -> string
   19.28    val extern_class: theory -> string -> xstring
   19.29    val intern_type: theory -> xstring -> string
   19.30 @@ -137,7 +137,7 @@
   19.31  (** datatype sign **)
   19.32  
   19.33  datatype sign = Sign of
   19.34 - {naming: NameSpace.naming,     (*common naming conventions*)
   19.35 + {naming: Name_Space.naming,    (*common naming conventions*)
   19.36    syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   19.37    tsig: Type.tsig,              (*order-sorted signature of types*)
   19.38    consts: Consts.T};            (*polymorphic constants*)
   19.39 @@ -150,17 +150,17 @@
   19.40    type T = sign;
   19.41    val copy = I;
   19.42    fun extend (Sign {syn, tsig, consts, ...}) =
   19.43 -    make_sign (NameSpace.default_naming, syn, tsig, consts);
   19.44 +    make_sign (Name_Space.default_naming, syn, tsig, consts);
   19.45  
   19.46    val empty =
   19.47 -    make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
   19.48 +    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
   19.49  
   19.50    fun merge pp (sign1, sign2) =
   19.51      let
   19.52        val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   19.53        val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   19.54  
   19.55 -      val naming = NameSpace.default_naming;
   19.56 +      val naming = Name_Space.default_naming;
   19.57        val syn = Syntax.merge_syntaxes syn1 syn2;
   19.58        val tsig = Type.merge_tsigs pp (tsig1, tsig2);
   19.59        val consts = Consts.merge (consts1, consts2);
   19.60 @@ -182,10 +182,10 @@
   19.61  
   19.62  val naming_of = #naming o rep_sg;
   19.63  
   19.64 -val full_name = NameSpace.full_name o naming_of;
   19.65 -fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
   19.66 +val full_name = Name_Space.full_name o naming_of;
   19.67 +fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
   19.68  
   19.69 -fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
   19.70 +fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
   19.71  fun full_bname_path thy path = full_name_path thy path o Binding.name;
   19.72  
   19.73  
   19.74 @@ -240,12 +240,12 @@
   19.75  val type_space = #1 o #types o Type.rep_tsig o tsig_of;
   19.76  val const_space = Consts.space_of o consts_of;
   19.77  
   19.78 -val intern_class = NameSpace.intern o class_space;
   19.79 -val extern_class = NameSpace.extern o class_space;
   19.80 -val intern_type = NameSpace.intern o type_space;
   19.81 -val extern_type = NameSpace.extern o type_space;
   19.82 -val intern_const = NameSpace.intern o const_space;
   19.83 -val extern_const = NameSpace.extern o const_space;
   19.84 +val intern_class = Name_Space.intern o class_space;
   19.85 +val extern_class = Name_Space.extern o class_space;
   19.86 +val intern_type = Name_Space.intern o type_space;
   19.87 +val extern_type = Name_Space.extern o type_space;
   19.88 +val intern_const = Name_Space.intern o const_space;
   19.89 +val extern_const = Name_Space.extern o const_space;
   19.90  
   19.91  val intern_sort = map o intern_class;
   19.92  val extern_sort = map o extern_class;
   19.93 @@ -612,10 +612,10 @@
   19.94  
   19.95  (* naming *)
   19.96  
   19.97 -val add_path = map_naming o NameSpace.add_path;
   19.98 -val root_path = map_naming NameSpace.root_path;
   19.99 -val parent_path = map_naming NameSpace.parent_path;
  19.100 -val mandatory_path = map_naming o NameSpace.mandatory_path;
  19.101 +val add_path = map_naming o Name_Space.add_path;
  19.102 +val root_path = map_naming Name_Space.root_path;
  19.103 +val parent_path = map_naming Name_Space.parent_path;
  19.104 +val mandatory_path = map_naming o Name_Space.mandatory_path;
  19.105  
  19.106  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
  19.107  
    20.1 --- a/src/Pure/simplifier.ML	Sat Oct 24 19:24:50 2009 +0200
    20.2 +++ b/src/Pure/simplifier.ML	Sat Oct 24 19:47:37 2009 +0200
    20.3 @@ -147,10 +147,10 @@
    20.4  
    20.5  structure Simprocs = GenericDataFun
    20.6  (
    20.7 -  type T = simproc NameSpace.table;
    20.8 -  val empty = NameSpace.empty_table;
    20.9 +  type T = simproc Name_Space.table;
   20.10 +  val empty = Name_Space.empty_table;
   20.11    val extend = I;
   20.12 -  fun merge _ simprocs = NameSpace.merge_tables simprocs;
   20.13 +  fun merge _ simprocs = Name_Space.merge_tables simprocs;
   20.14  );
   20.15  
   20.16  
   20.17 @@ -159,7 +159,7 @@
   20.18  fun get_simproc context xname =
   20.19    let
   20.20      val (space, tab) = Simprocs.get context;
   20.21 -    val name = NameSpace.intern space xname;
   20.22 +    val name = Name_Space.intern space xname;
   20.23    in
   20.24      (case Symtab.lookup tab name of
   20.25        SOME proc => proc
   20.26 @@ -197,7 +197,7 @@
   20.27          val b' = Morphism.binding phi b;
   20.28          val simproc' = morph_simproc phi simproc;
   20.29        in
   20.30 -        Simprocs.map (#2 o NameSpace.define true naming (b', simproc'))
   20.31 +        Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))
   20.32          #> map_ss (fn ss => ss addsimprocs [simproc'])
   20.33        end)
   20.34    end;
    21.1 --- a/src/Pure/theory.ML	Sat Oct 24 19:24:50 2009 +0200
    21.2 +++ b/src/Pure/theory.ML	Sat Oct 24 19:47:37 2009 +0200
    21.3 @@ -19,7 +19,7 @@
    21.4    val checkpoint: theory -> theory
    21.5    val copy: theory -> theory
    21.6    val requires: theory -> string -> string -> unit
    21.7 -  val axiom_space: theory -> NameSpace.T
    21.8 +  val axiom_space: theory -> Name_Space.T
    21.9    val axiom_table: theory -> term Symtab.table
   21.10    val axioms_of: theory -> (string * term) list
   21.11    val all_axioms_of: theory -> (string * term) list
   21.12 @@ -80,7 +80,7 @@
   21.13    perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
   21.14  
   21.15  datatype thy = Thy of
   21.16 - {axioms: term NameSpace.table,
   21.17 + {axioms: term Name_Space.table,
   21.18    defs: Defs.T,
   21.19    wrappers: wrapper list * wrapper list};
   21.20  
   21.21 @@ -89,18 +89,18 @@
   21.22  structure ThyData = TheoryDataFun
   21.23  (
   21.24    type T = thy;
   21.25 -  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
   21.26 +  val empty = make_thy (Name_Space.empty_table, Defs.empty, ([], []));
   21.27    val copy = I;
   21.28  
   21.29    fun extend (Thy {axioms = _, defs, wrappers}) =
   21.30 -    make_thy (NameSpace.empty_table, defs, wrappers);
   21.31 +    make_thy (Name_Space.empty_table, defs, wrappers);
   21.32  
   21.33    fun merge pp (thy1, thy2) =
   21.34      let
   21.35        val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   21.36        val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   21.37  
   21.38 -      val axioms' = NameSpace.empty_table;
   21.39 +      val axioms' = Name_Space.empty_table;
   21.40        val defs' = Defs.merge pp (defs1, defs2);
   21.41        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   21.42        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   21.43 @@ -174,7 +174,7 @@
   21.44  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   21.45    let
   21.46      val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
   21.47 -    val axioms' = fold (#2 oo NameSpace.define true (Sign.naming_of thy)) axms axioms;
   21.48 +    val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
   21.49    in axioms' end);
   21.50  
   21.51  in
    22.1 --- a/src/Pure/thm.ML	Sat Oct 24 19:24:50 2009 +0200
    22.2 +++ b/src/Pure/thm.ML	Sat Oct 24 19:47:37 2009 +0200
    22.3 @@ -1726,19 +1726,19 @@
    22.4  
    22.5  structure Oracles = TheoryDataFun
    22.6  (
    22.7 -  type T = unit NameSpace.table;
    22.8 -  val empty = NameSpace.empty_table;
    22.9 +  type T = unit Name_Space.table;
   22.10 +  val empty = Name_Space.empty_table;
   22.11    val copy = I;
   22.12    val extend = I;
   22.13 -  fun merge _ oracles : T = NameSpace.merge_tables oracles;
   22.14 +  fun merge _ oracles : T = Name_Space.merge_tables oracles;
   22.15  );
   22.16  
   22.17 -val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
   22.18 +val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
   22.19  
   22.20  fun add_oracle (b, oracle) thy =
   22.21    let
   22.22      val naming = Sign.naming_of thy;
   22.23 -    val (name, tab') = NameSpace.define true naming (b, ()) (Oracles.get thy);
   22.24 +    val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy);
   22.25      val thy' = Oracles.put tab' thy;
   22.26    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
   22.27  
    23.1 --- a/src/Pure/type.ML	Sat Oct 24 19:24:50 2009 +0200
    23.2 +++ b/src/Pure/type.ML	Sat Oct 24 19:47:37 2009 +0200
    23.3 @@ -14,9 +14,9 @@
    23.4      Nonterminal
    23.5    type tsig
    23.6    val rep_tsig: tsig ->
    23.7 -   {classes: NameSpace.T * Sorts.algebra,
    23.8 +   {classes: Name_Space.T * Sorts.algebra,
    23.9      default: sort,
   23.10 -    types: (decl * Properties.T) NameSpace.table,
   23.11 +    types: (decl * Properties.T) Name_Space.table,
   23.12      log_types: string list}
   23.13    val empty_tsig: tsig
   23.14    val defaultS: tsig -> sort
   23.15 @@ -70,12 +70,12 @@
   23.16    val eq_type: tyenv -> typ * typ -> bool
   23.17  
   23.18    (*extend and merge type signatures*)
   23.19 -  val add_class: Pretty.pp -> NameSpace.naming -> binding * class list -> tsig -> tsig
   23.20 +  val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
   23.21    val hide_class: bool -> string -> tsig -> tsig
   23.22    val set_defsort: sort -> tsig -> tsig
   23.23 -  val add_type: NameSpace.naming -> Properties.T -> binding * int -> tsig -> tsig
   23.24 -  val add_abbrev: NameSpace.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
   23.25 -  val add_nonterminal: NameSpace.naming -> Properties.T -> binding -> tsig -> tsig
   23.26 +  val add_type: Name_Space.naming -> Properties.T -> binding * int -> tsig -> tsig
   23.27 +  val add_abbrev: Name_Space.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
   23.28 +  val add_nonterminal: Name_Space.naming -> Properties.T -> binding -> tsig -> tsig
   23.29    val hide_type: bool -> string -> tsig -> tsig
   23.30    val add_arity: Pretty.pp -> arity -> tsig -> tsig
   23.31    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   23.32 @@ -99,9 +99,9 @@
   23.33  
   23.34  datatype tsig =
   23.35    TSig of {
   23.36 -    classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
   23.37 +    classes: Name_Space.T * Sorts.algebra,  (*order-sorted algebra of type classes*)
   23.38      default: sort,                          (*default sort on input*)
   23.39 -    types: (decl * Properties.T) NameSpace.table,  (*declared types*)
   23.40 +    types: (decl * Properties.T) Name_Space.table,  (*declared types*)
   23.41      log_types: string list};                (*logical types sorted by number of arguments*)
   23.42  
   23.43  fun rep_tsig (TSig comps) = comps;
   23.44 @@ -120,7 +120,7 @@
   23.45    build_tsig (f (classes, default, types));
   23.46  
   23.47  val empty_tsig =
   23.48 -  build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
   23.49 +  build_tsig ((Name_Space.empty, Sorts.empty_algebra), [], Name_Space.empty_table);
   23.50  
   23.51  
   23.52  (* classes and sorts *)
   23.53 @@ -511,12 +511,12 @@
   23.54      let
   23.55        val cs' = map (cert_class tsig) cs
   23.56          handle TYPE (msg, _, _) => error msg;
   23.57 -      val (c', space') = space |> NameSpace.declare true naming c;
   23.58 +      val (c', space') = space |> Name_Space.declare true naming c;
   23.59        val classes' = classes |> Sorts.add_class pp (c', cs');
   23.60      in ((space', classes'), default, types) end);
   23.61  
   23.62  fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
   23.63 -  ((NameSpace.hide fully c space, classes), default, types));
   23.64 +  ((Name_Space.hide fully c space, classes), default, types));
   23.65  
   23.66  
   23.67  (* arities *)
   23.68 @@ -558,13 +558,13 @@
   23.69  fun new_decl naming tags (c, decl) types =
   23.70    let
   23.71      val tags' = tags |> Position.default_properties (Position.thread_data ());
   23.72 -    val (_, types') = NameSpace.define true naming (c, (decl, tags')) types;
   23.73 +    val (_, types') = Name_Space.define true naming (c, (decl, tags')) types;
   23.74    in types' end;
   23.75  
   23.76  fun map_types f = map_tsig (fn (classes, default, types) =>
   23.77    let
   23.78      val (space', tab') = f types;
   23.79 -    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
   23.80 +    val _ = Name_Space.intern space' "dummy" = "dummy" orelse
   23.81        error "Illegal declaration of dummy type";
   23.82    in (classes, default, (space', tab')) end);
   23.83  
   23.84 @@ -600,7 +600,7 @@
   23.85  end;
   23.86  
   23.87  fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
   23.88 -  (classes, default, (NameSpace.hide fully c space, types)));
   23.89 +  (classes, default, (Name_Space.hide fully c space, types)));
   23.90  
   23.91  
   23.92  (* merge type signatures *)
   23.93 @@ -612,10 +612,10 @@
   23.94      val (TSig {classes = (space2, classes2), default = default2, types = types2,
   23.95        log_types = _}) = tsig2;
   23.96  
   23.97 -    val space' = NameSpace.merge (space1, space2);
   23.98 +    val space' = Name_Space.merge (space1, space2);
   23.99      val classes' = Sorts.merge_algebra pp (classes1, classes2);
  23.100      val default' = Sorts.inter_sort classes' (default1, default2);
  23.101 -    val types' = NameSpace.merge_tables (types1, types2);
  23.102 +    val types' = Name_Space.merge_tables (types1, types2);
  23.103    in build_tsig ((space', classes'), default', types') end;
  23.104  
  23.105  end;