renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

--- a/src/HOL/Tools/inductive.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -144,7 +144,7 @@
     val (tab, monos) = get_inductives ctxt;
     val space = Consts.space_of (ProofContext.consts_of ctxt);
   in
-    [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))),
+    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
     |> Pretty.chunks |> Pretty.writeln
   end;

--- a/src/HOL/Tools/record.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -1810,7 +1810,7 @@
 
 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
   let
-    val external_names = NameSpace.external_names (Sign.naming_of thy);
+    val external_names = Name_Space.external_names (Sign.naming_of thy);
 
     val alphas = map fst args;
     val name = Sign.full_bname thy bname;

--- a/src/HOL/Tools/res_atp.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -355,7 +355,7 @@
     if run_blacklist_filter andalso is_package_def name then I
     else
       let val xname = Facts.extern facts name in
-        if NameSpace.is_hidden xname then I
+        if Name_Space.is_hidden xname then I
         else cons (xname, filter_out ResAxioms.bad_for_atp ths)
       end) facts [];
 

--- a/src/Pure/General/name_space.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/General/name_space.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -46,7 +46,7 @@
   val extern_table: 'a table -> (xstring * 'a) list
 end;
 
-structure NameSpace: NAME_SPACE =
+structure Name_Space: NAME_SPACE =
 struct
 
 
@@ -79,13 +79,13 @@
 (* datatype T *)
 
 datatype T =
-  NameSpace of
+  Name_Space of
     (string list * string list) Symtab.table *   (*internals, hidden internals*)
     entry Symtab.table;
 
-val empty = NameSpace (Symtab.empty, Symtab.empty);
+val empty = Name_Space (Symtab.empty, Symtab.empty);
 
-fun lookup (NameSpace (tab, _)) xname =
+fun lookup (Name_Space (tab, _)) xname =
   (case Symtab.lookup tab xname of
     NONE => (xname, true)
   | SOME ([], []) => (xname, true)
@@ -93,12 +93,12 @@
   | SOME (name :: _, _) => (name, false)
   | SOME ([], name' :: _) => (hidden name', true));
 
-fun get_accesses (NameSpace (_, entries)) name =
+fun get_accesses (Name_Space (_, entries)) name =
   (case Symtab.lookup entries name of
     NONE => [name]
   | SOME {externals, ...} => externals);
 
-fun valid_accesses (NameSpace (tab, _)) name =
+fun valid_accesses (Name_Space (tab, _)) name =
   Symtab.fold (fn (xname, (names, _)) =>
     if not (null names) andalso hd names = name then cons xname else I) tab [];
 
@@ -136,8 +136,8 @@
 
 local
 
-fun map_space f xname (NameSpace (tab, entries)) =
-  NameSpace (Symtab.map_default (xname, ([], [])) f tab, entries);
+fun map_space f xname (Name_Space (tab, entries)) =
+  Name_Space (Symtab.map_default (xname, ([], [])) f tab, entries);
 
 in
 
@@ -168,7 +168,7 @@
 
 (* merge *)
 
-fun merge (NameSpace (tab1, entries1), NameSpace (tab2, entries2)) =
+fun merge (Name_Space (tab1, entries1), Name_Space (tab2, entries2)) =
   let
     val tab' = (tab1, tab2) |> Symtab.join
       (K (fn ((names1, names1'), (names2, names2')) =>
@@ -182,7 +182,7 @@
           error ("Duplicate declaration " ^
             quote (str_of_entry true (name, entry1)) ^ " vs. " ^
             quote (str_of_entry true (name, entry2))));
-  in NameSpace (tab', entries') end;
+  in Name_Space (tab', entries') end;
 
 
 
@@ -245,13 +245,13 @@
 
 (* declaration *)
 
-fun new_entry strict entry (NameSpace (tab, entries)) =
+fun new_entry strict entry (Name_Space (tab, entries)) =
   let
     val entries' =
       (if strict then Symtab.update_new else Symtab.update) entry entries
         handle Symtab.DUP _ =>
           error ("Duplicate declaration " ^ quote (str_of_entry true entry));
-  in NameSpace (tab, entries') end;
+  in Name_Space (tab, entries') end;
 
 fun declare strict naming binding space =
   let
@@ -294,6 +294,6 @@
 
 end;
 
-structure Basic_Name_Space: BASIC_NAME_SPACE = NameSpace;
+structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
 open Basic_Name_Space;
 

--- a/src/Pure/Isar/attrib.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -67,11 +67,11 @@
 
 structure Attributes = TheoryDataFun
 (
-  type T = ((src -> attribute) * string) NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = ((src -> attribute) * string) Name_Space.table;
+  val empty = Name_Space.empty_table;
   val copy = I;
   val extend = I;
-  fun merge _ tables : T = NameSpace.merge_tables tables;
+  fun merge _ tables : T = Name_Space.merge_tables tables;
 );
 
 fun print_attributes thy =
@@ -80,20 +80,20 @@
     fun prt_attr (name, (_, comment)) = Pretty.block
       [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
-    [Pretty.big_list "attributes:" (map prt_attr (NameSpace.extern_table attribs))]
+    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
 fun add_attribute name att comment thy = thy
-  |> Attributes.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (att, comment)));
+  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
 
 
 (* name space *)
 
-val intern = NameSpace.intern o #1 o Attributes.get;
+val intern = Name_Space.intern o #1 o Attributes.get;
 val intern_src = Args.map_name o intern;
 
-val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
+val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
 
 
 (* pretty printing *)
@@ -338,7 +338,7 @@
         Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
           Pretty.str (Config.print_value value)]
       end;
-    val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
+    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
 

--- a/src/Pure/Isar/isar_cmd.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -400,7 +400,7 @@
     val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
     val {classes, ...} = Sorts.rep_algebra algebra;
     fun entry (c, (i, (_, cs))) =
-      (i, {name = NameSpace.extern space c, ID = c, parents = cs,
+      (i, {name = Name_Space.extern space c, ID = c, parents = cs,
             dir = "", unfold = true, path = ""});
     val gr =
       Graph.fold (cons o entry) classes []

--- a/src/Pure/Isar/local_theory.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -17,7 +17,7 @@
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val checkpoint: local_theory -> local_theory
-  val full_naming: local_theory -> NameSpace.naming
+  val full_naming: local_theory -> Name_Space.naming
   val full_name: local_theory -> binding -> string
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
@@ -139,9 +139,9 @@
 
 fun full_naming lthy =
   Sign.naming_of (ProofContext.theory_of lthy)
-  |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
+  |> Name_Space.mandatory_path (#theory_prefix (get_lthy lthy));
 
-fun full_name naming = NameSpace.full_name (full_naming naming);
+fun full_name naming = Name_Space.full_name (full_naming naming);
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))

--- a/src/Pure/Isar/locale.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -124,15 +124,15 @@
 
 structure Locales = TheoryDataFun
 (
-  type T = locale NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = locale Name_Space.table;
+  val empty = Name_Space.empty_table;
   val copy = I;
   val extend = I;
-  fun merge _ = NameSpace.join_tables (K merge_locale);
+  fun merge _ = Name_Space.join_tables (K merge_locale);
 );
 
-val intern = NameSpace.intern o #1 o Locales.get;
-val extern = NameSpace.extern o #1 o Locales.get;
+val intern = Name_Space.intern o #1 o Locales.get;
+val extern = Name_Space.extern o #1 o Locales.get;
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
 val defined = Symtab.defined o #2 o Locales.get;
@@ -143,7 +143,7 @@
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
-  thy |> Locales.map (NameSpace.define true (Sign.naming_of thy)
+  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
@@ -153,7 +153,7 @@
   Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
 
 fun print_locales thy =
-  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (Locales.get thy)))
+  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   |> Pretty.writeln;
 
 

--- a/src/Pure/Isar/method.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -322,11 +322,11 @@
 
 structure Methods = TheoryDataFun
 (
-  type T = ((src -> Proof.context -> method) * string) NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = ((src -> Proof.context -> method) * string) Name_Space.table;
+  val empty = Name_Space.empty_table;
   val copy = I;
   val extend = I;
-  fun merge _ tables : T = NameSpace.merge_tables tables;
+  fun merge _ tables : T = Name_Space.merge_tables tables;
 );
 
 fun print_methods thy =
@@ -335,17 +335,17 @@
     fun prt_meth (name, (_, comment)) = Pretty.block
       [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
-    [Pretty.big_list "methods:" (map prt_meth (NameSpace.extern_table meths))]
+    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
 fun add_method name meth comment thy = thy
-  |> Methods.map (#2 o NameSpace.define true (Sign.naming_of thy) (name, (meth, comment)));
+  |> Methods.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (meth, comment)));
 
 
 (* get methods *)
 
-val intern = NameSpace.intern o #1 o Methods.get;
+val intern = Name_Space.intern o #1 o Methods.get;
 val defined = Symtab.defined o #2 o Methods.get;
 
 fun method_i thy =
@@ -359,7 +359,7 @@
       end;
   in meth end;
 
-fun method thy = method_i thy o Args.map_name (NameSpace.intern (#1 (Methods.get thy)));
+fun method thy = method_i thy o Args.map_name (Name_Space.intern (#1 (Methods.get thy)));
 
 
 (* method setup *)

--- a/src/Pure/Isar/proof_context.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -21,7 +21,7 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
-  val naming_of: Proof.context -> NameSpace.naming
+  val naming_of: Proof.context -> Name_Space.naming
   val full_name: Proof.context -> binding -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
@@ -170,7 +170,7 @@
 datatype ctxt =
   Ctxt of
    {mode: mode,                                       (*inner syntax mode*)
-    naming: NameSpace.naming,                         (*local naming conventions*)
+    naming: Name_Space.naming,                        (*local naming conventions*)
     syntax: LocalSyntax.T,                            (*local syntax*)
     consts: Consts.T * Consts.T,                      (*local/global consts*)
     facts: Facts.T,                                   (*local facts*)
@@ -180,7 +180,7 @@
   Ctxt {mode = mode, naming = naming, syntax = syntax,
     consts = consts, facts = facts, cases = cases};
 
-val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
+val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
 
 structure ContextData = ProofDataFun
 (
@@ -231,7 +231,7 @@
   map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
 
 val naming_of = #naming o rep_context;
-val full_name = NameSpace.full_name o naming_of;
+val full_name = Name_Space.full_name o naming_of;
 
 val syntax_of = #syntax o rep_context;
 val syn_of = LocalSyntax.syn_of o syntax_of;
@@ -924,10 +924,10 @@
 
 (* name space operations *)
 
-val add_path        = map_naming o NameSpace.add_path;
-val mandatory_path  = map_naming o NameSpace.mandatory_path;
-val restore_naming  = map_naming o K o naming_of;
-val reset_naming    = map_naming (K local_naming);
+val add_path = map_naming o Name_Space.add_path;
+val mandatory_path = map_naming o Name_Space.mandatory_path;
+val restore_naming = map_naming o K o naming_of;
+val reset_naming = map_naming (K local_naming);
 
 
 (* facts *)
@@ -1230,7 +1230,7 @@
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
-    val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
+    val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
   in
     if null abbrevs andalso not (! verbose) then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]

--- a/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -420,9 +420,9 @@
   ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
   ("show_structs", setmp_CRITICAL show_structs o boolean),
   ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
-  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
-  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
-  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
+  ("long_names", setmp_CRITICAL Name_Space.long_names o boolean),
+  ("short_names", setmp_CRITICAL Name_Space.short_names o boolean),
+  ("unique_names", setmp_CRITICAL Name_Space.unique_names o boolean),
   ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   ("display", setmp_CRITICAL display o boolean),
   ("break", setmp_CRITICAL break o boolean),

--- a/src/Pure/Tools/find_theorems.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -326,7 +326,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
+val hidden_ord = bool_ord o pairself Name_Space.is_hidden;
 val qual_ord = int_ord o pairself (length o Long_Name.explode);
 val txt_ord = int_ord o pairself size;
 
@@ -355,7 +355,8 @@
     val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
 
     val shorten =
-      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
+      Name_Space.extern_flags
+        {long_names = false, short_names = false, unique_names = false} space;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)

--- a/src/Pure/consts.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/consts.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -11,15 +11,15 @@
   val eq_consts: T * T -> bool
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
-   {constants: (typ * term option) NameSpace.table,
-    constraints: typ NameSpace.table}
+   {constants: (typ * term option) Name_Space.table,
+    constraints: typ Name_Space.table}
   val the_type: T -> string -> typ                             (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
   val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
-  val space_of: T -> NameSpace.T
+  val space_of: T -> Name_Space.T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_early: T -> string -> xstring
@@ -29,9 +29,9 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
+  val declare: bool -> Name_Space.naming -> Properties.T -> (binding * typ) -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
+  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
     binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
@@ -50,7 +50,7 @@
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
 
 datatype T = Consts of
- {decls: (decl * abbrev option) NameSpace.table,
+ {decls: (decl * abbrev option) Name_Space.table,
   constraints: typ Symtab.table,
   rev_abbrevs: (term * term) Item_Net.T Symtab.table};
 
@@ -123,8 +123,8 @@
 
 fun space_of (Consts {decls = (space, _), ...}) = space;
 
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
 
 fun extern_early consts c =
   (case try (the_const consts) c of
@@ -224,7 +224,7 @@
 (* name space *)
 
 fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
-  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs));
+  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
 
 
 (* declarations *)
@@ -234,7 +234,7 @@
     let
       val tags' = tags |> Position.default_properties (Position.thread_data ());
       val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
-      val (_, decls') = decls |> NameSpace.define true naming (b, (decl, NONE));
+      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
 
@@ -280,7 +280,7 @@
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
-    val lhs = Const (NameSpace.full_name naming b, T);
+    val lhs = Const (Name_Space.full_name naming b, T);
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
@@ -288,7 +288,7 @@
         val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val (_, decls') = decls
-          |> NameSpace.define true naming (b, (decl, SOME abbr));
+          |> Name_Space.define true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
           |> insert_abbrevs mode (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
@@ -307,13 +307,13 @@
 
 (* empty and merge *)
 
-val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
+val empty = make_consts (Name_Space.empty_table, Symtab.empty, Symtab.empty);
 
 fun merge
    (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
     Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
   let
-    val decls' = NameSpace.merge_tables (decls1, decls2);
+    val decls' = Name_Space.merge_tables (decls1, decls2);
     val constraints' = Symtab.join (K fst) (constraints1, constraints2);
     val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
   in make_consts (decls', constraints', rev_abbrevs') end;

--- a/src/Pure/display.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/display.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -179,25 +179,25 @@
     val {restricts, reducts} = Defs.dest defs;
     val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
-    val extern_const = NameSpace.extern (#1 constants);
+    val extern_const = Name_Space.extern (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
     val {classes, arities} = Sorts.rep_algebra class_algebra;
 
-    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
-    val tdecls = NameSpace.dest_table types;
-    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
+    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
+    val tdecls = Name_Space.dest_table types;
+    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
 
     fun prune_const c = not verbose andalso
       member (op =) (Consts.the_tags consts c) Markup.property_internal;
-    val cnsts = NameSpace.extern_table (#1 constants,
+    val cnsts = Name_Space.extern_table (#1 constants,
       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = NameSpace.extern_table constraints;
+    val cnstrs = Name_Space.extern_table constraints;
 
-    val axms = NameSpace.extern_table axioms;
+    val axms = Name_Space.extern_table axioms;
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>

--- a/src/Pure/drule.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/drule.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -452,7 +452,7 @@
 
 val read_prop = certify o SimpleSyntax.read_prop;
 
-fun get_def thy = Thm.axiom thy o NameSpace.intern (Theory.axiom_space thy) o Thm.def_name;
+fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name;
 
 fun store_thm name th =
   Context.>>> (Context.map_theory_result (PureThy.store_thm (Binding.name name, th)));

--- a/src/Pure/facts.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/facts.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -20,7 +20,7 @@
   val selections: string * thm list -> (ref * thm) list
   type T
   val empty: T
-  val space_of: T -> NameSpace.T
+  val space_of: T -> Name_Space.T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
@@ -31,9 +31,9 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
-  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
-  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
+  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
+  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
+  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
 end;
@@ -122,11 +122,11 @@
 datatype fact = Static of thm list | Dynamic of Context.generic -> thm list;
 
 datatype T = Facts of
- {facts: fact NameSpace.table,
+ {facts: fact Name_Space.table,
   props: thm Net.net};
 
 fun make_facts facts props = Facts {facts = facts, props = props};
-val empty = make_facts NameSpace.empty_table Net.empty;
+val empty = make_facts Name_Space.empty_table Net.empty;
 
 
 (* named facts *)
@@ -136,8 +136,8 @@
 val space_of = #1 o facts_of;
 val table_of = #2 o facts_of;
 
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
 
 val defined = Symtab.defined o table_of;
 
@@ -177,7 +177,7 @@
 
 fun merge (Facts {facts = facts1, props = props1}, Facts {facts = facts2, props = props2}) =
   let
-    val facts' = NameSpace.merge_tables (facts1, facts2);
+    val facts' = Name_Space.merge_tables (facts1, facts2);
     val props' = Net.merge (is_equal o prop_ord) (props1, props2);
   in make_facts facts' props' end;
 
@@ -190,7 +190,7 @@
   let
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
-      else NameSpace.define strict naming (b, Static ths) facts;
+      else Name_Space.define strict naming (b, Static ths) facts;
     val props' =
       if do_props
       then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
@@ -208,7 +208,7 @@
 (* add dynamic entries *)
 
 fun add_dynamic naming (b, f) (Facts {facts, props}) =
-  let val (name, facts') = NameSpace.define true naming (b, Dynamic f) facts;
+  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
   in (name, make_facts facts' props) end;
 
 
@@ -216,11 +216,11 @@
 
 fun del name (Facts {facts = (space, tab), props}) =
   let
-    val space' = NameSpace.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
+    val space' = Name_Space.hide true name space handle ERROR _ => space;  (* FIXME handle?? *)
     val tab' = Symtab.delete_safe name tab;
   in make_facts (space', tab') props end;
 
 fun hide fully name (Facts {facts = (space, tab), props}) =
-  make_facts (NameSpace.hide fully name space, tab) props;
+  make_facts (Name_Space.hide fully name space, tab) props;
 
 end;

--- a/src/Pure/name.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/name.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -45,7 +45,7 @@
 
 (* checked binding *)
 
-val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
+val of_binding = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
 
 
 (* encoded bounds *)

--- a/src/Pure/pure_thy.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/pure_thy.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -146,7 +146,7 @@
   else
     let
       val naming = Sign.naming_of thy;
-      val name = NameSpace.full_name naming b;
+      val name = Name_Space.full_name naming b;
       val (thy', thms') =
         register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
       val thms'' = map (Thm.transfer thy') thms';

--- a/src/Pure/sign.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/sign.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -8,11 +8,11 @@
 signature SIGN =
 sig
   val rep_sg: theory ->
-   {naming: NameSpace.naming,
+   {naming: Name_Space.naming,
     syn: Syntax.syntax,
     tsig: Type.tsig,
     consts: Consts.T}
-  val naming_of: theory -> NameSpace.naming
+  val naming_of: theory -> Name_Space.naming
   val full_name: theory -> binding -> string
   val full_name_path: theory -> string -> binding -> string
   val full_bname: theory -> bstring -> string
@@ -44,9 +44,9 @@
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
   val mk_const: theory -> string * typ list -> term
-  val class_space: theory -> NameSpace.T
-  val type_space: theory -> NameSpace.T
-  val const_space: theory -> NameSpace.T
+  val class_space: theory -> Name_Space.T
+  val type_space: theory -> Name_Space.T
+  val const_space: theory -> Name_Space.T
   val intern_class: theory -> xstring -> string
   val extern_class: theory -> string -> xstring
   val intern_type: theory -> xstring -> string
@@ -137,7 +137,7 @@
 (** datatype sign **)
 
 datatype sign = Sign of
- {naming: NameSpace.naming,     (*common naming conventions*)
+ {naming: Name_Space.naming,    (*common naming conventions*)
   syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   tsig: Type.tsig,              (*order-sorted signature of types*)
   consts: Consts.T};            (*polymorphic constants*)
@@ -150,17 +150,17 @@
   type T = sign;
   val copy = I;
   fun extend (Sign {syn, tsig, consts, ...}) =
-    make_sign (NameSpace.default_naming, syn, tsig, consts);
+    make_sign (Name_Space.default_naming, syn, tsig, consts);
 
   val empty =
-    make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
 
   fun merge pp (sign1, sign2) =
     let
       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
 
-      val naming = NameSpace.default_naming;
+      val naming = Name_Space.default_naming;
       val syn = Syntax.merge_syntaxes syn1 syn2;
       val tsig = Type.merge_tsigs pp (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
@@ -182,10 +182,10 @@
 
 val naming_of = #naming o rep_sg;
 
-val full_name = NameSpace.full_name o naming_of;
-fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
+val full_name = Name_Space.full_name o naming_of;
+fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
 
-fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
+fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
 fun full_bname_path thy path = full_name_path thy path o Binding.name;
 
 
@@ -240,12 +240,12 @@
 val type_space = #1 o #types o Type.rep_tsig o tsig_of;
 val const_space = Consts.space_of o consts_of;
 
-val intern_class = NameSpace.intern o class_space;
-val extern_class = NameSpace.extern o class_space;
-val intern_type = NameSpace.intern o type_space;
-val extern_type = NameSpace.extern o type_space;
-val intern_const = NameSpace.intern o const_space;
-val extern_const = NameSpace.extern o const_space;
+val intern_class = Name_Space.intern o class_space;
+val extern_class = Name_Space.extern o class_space;
+val intern_type = Name_Space.intern o type_space;
+val extern_type = Name_Space.extern o type_space;
+val intern_const = Name_Space.intern o const_space;
+val extern_const = Name_Space.extern o const_space;
 
 val intern_sort = map o intern_class;
 val extern_sort = map o extern_class;
@@ -612,10 +612,10 @@
 
 (* naming *)
 
-val add_path = map_naming o NameSpace.add_path;
-val root_path = map_naming NameSpace.root_path;
-val parent_path = map_naming NameSpace.parent_path;
-val mandatory_path = map_naming o NameSpace.mandatory_path;
+val add_path = map_naming o Name_Space.add_path;
+val root_path = map_naming Name_Space.root_path;
+val parent_path = map_naming Name_Space.parent_path;
+val mandatory_path = map_naming o Name_Space.mandatory_path;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 

--- a/src/Pure/simplifier.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -147,10 +147,10 @@
 
 structure Simprocs = GenericDataFun
 (
-  type T = simproc NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = simproc Name_Space.table;
+  val empty = Name_Space.empty_table;
   val extend = I;
-  fun merge _ simprocs = NameSpace.merge_tables simprocs;
+  fun merge _ simprocs = Name_Space.merge_tables simprocs;
 );
 
 
@@ -159,7 +159,7 @@
 fun get_simproc context xname =
   let
     val (space, tab) = Simprocs.get context;
-    val name = NameSpace.intern space xname;
+    val name = Name_Space.intern space xname;
   in
     (case Symtab.lookup tab name of
       SOME proc => proc
@@ -197,7 +197,7 @@
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;
       in
-        Simprocs.map (#2 o NameSpace.define true naming (b', simproc'))
+        Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))
         #> map_ss (fn ss => ss addsimprocs [simproc'])
       end)
   end;

--- a/src/Pure/theory.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/theory.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -19,7 +19,7 @@
   val checkpoint: theory -> theory
   val copy: theory -> theory
   val requires: theory -> string -> string -> unit
-  val axiom_space: theory -> NameSpace.T
+  val axiom_space: theory -> Name_Space.T
   val axiom_table: theory -> term Symtab.table
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
@@ -80,7 +80,7 @@
   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
 
 datatype thy = Thy of
- {axioms: term NameSpace.table,
+ {axioms: term Name_Space.table,
   defs: Defs.T,
   wrappers: wrapper list * wrapper list};
 
@@ -89,18 +89,18 @@
 structure ThyData = TheoryDataFun
 (
   type T = thy;
-  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
+  val empty = make_thy (Name_Space.empty_table, Defs.empty, ([], []));
   val copy = I;
 
   fun extend (Thy {axioms = _, defs, wrappers}) =
-    make_thy (NameSpace.empty_table, defs, wrappers);
+    make_thy (Name_Space.empty_table, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
       val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
-      val axioms' = NameSpace.empty_table;
+      val axioms' = Name_Space.empty_table;
       val defs' = Defs.merge pp (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
@@ -174,7 +174,7 @@
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
     val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
-    val axioms' = fold (#2 oo NameSpace.define true (Sign.naming_of thy)) axms axioms;
+    val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
   in axioms' end);
 
 in

--- a/src/Pure/thm.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/thm.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -1726,19 +1726,19 @@
 
 structure Oracles = TheoryDataFun
 (
-  type T = unit NameSpace.table;
-  val empty = NameSpace.empty_table;
+  type T = unit Name_Space.table;
+  val empty = Name_Space.empty_table;
   val copy = I;
   val extend = I;
-  fun merge _ oracles : T = NameSpace.merge_tables oracles;
+  fun merge _ oracles : T = Name_Space.merge_tables oracles;
 );
 
-val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get;
+val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
 
 fun add_oracle (b, oracle) thy =
   let
     val naming = Sign.naming_of thy;
-    val (name, tab') = NameSpace.define true naming (b, ()) (Oracles.get thy);
+    val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy);
     val thy' = Oracles.put tab' thy;
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
 

--- a/src/Pure/type.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/type.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -14,9 +14,9 @@
     Nonterminal
   type tsig
   val rep_tsig: tsig ->
-   {classes: NameSpace.T * Sorts.algebra,
+   {classes: Name_Space.T * Sorts.algebra,
     default: sort,
-    types: (decl * Properties.T) NameSpace.table,
+    types: (decl * Properties.T) Name_Space.table,
     log_types: string list}
   val empty_tsig: tsig
   val defaultS: tsig -> sort
@@ -70,12 +70,12 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Pretty.pp -> NameSpace.naming -> binding * class list -> tsig -> tsig
+  val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
-  val add_type: NameSpace.naming -> Properties.T -> binding * int -> tsig -> tsig
-  val add_abbrev: NameSpace.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
-  val add_nonterminal: NameSpace.naming -> Properties.T -> binding -> tsig -> tsig
+  val add_type: Name_Space.naming -> Properties.T -> binding * int -> tsig -> tsig
+  val add_abbrev: Name_Space.naming -> Properties.T -> binding * string list * typ -> tsig -> tsig
+  val add_nonterminal: Name_Space.naming -> Properties.T -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -99,9 +99,9 @@
 
 datatype tsig =
   TSig of {
-    classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
+    classes: Name_Space.T * Sorts.algebra,  (*order-sorted algebra of type classes*)
     default: sort,                          (*default sort on input*)
-    types: (decl * Properties.T) NameSpace.table,  (*declared types*)
+    types: (decl * Properties.T) Name_Space.table,  (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
 fun rep_tsig (TSig comps) = comps;
@@ -120,7 +120,7 @@
   build_tsig (f (classes, default, types));
 
 val empty_tsig =
-  build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
+  build_tsig ((Name_Space.empty, Sorts.empty_algebra), [], Name_Space.empty_table);
 
 
 (* classes and sorts *)
@@ -511,12 +511,12 @@
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
-      val (c', space') = space |> NameSpace.declare true naming c;
+      val (c', space') = space |> Name_Space.declare true naming c;
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
-  ((NameSpace.hide fully c space, classes), default, types));
+  ((Name_Space.hide fully c space, classes), default, types));
 
 
 (* arities *)
@@ -558,13 +558,13 @@
 fun new_decl naming tags (c, decl) types =
   let
     val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val (_, types') = NameSpace.define true naming (c, (decl, tags')) types;
+    val (_, types') = Name_Space.define true naming (c, (decl, tags')) types;
   in types' end;
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
     val (space', tab') = f types;
-    val _ = NameSpace.intern space' "dummy" = "dummy" orelse
+    val _ = Name_Space.intern space' "dummy" = "dummy" orelse
       error "Illegal declaration of dummy type";
   in (classes, default, (space', tab')) end);
 
@@ -600,7 +600,7 @@
 end;
 
 fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
-  (classes, default, (NameSpace.hide fully c space, types)));
+  (classes, default, (Name_Space.hide fully c space, types)));
 
 
 (* merge type signatures *)
@@ -612,10 +612,10 @@
     val (TSig {classes = (space2, classes2), default = default2, types = types2,
       log_types = _}) = tsig2;
 
-    val space' = NameSpace.merge (space1, space2);
+    val space' = Name_Space.merge (space1, space2);
     val classes' = Sorts.merge_algebra pp (classes1, classes2);
     val default' = Sorts.inter_sort classes' (default1, default2);
-    val types' = NameSpace.merge_tables (types1, types2);
+    val types' = Name_Space.merge_tables (types1, types2);
   in build_tsig ((space', classes'), default', types') end;
 
 end;