# HG changeset patch
# User wenzelm
# Date 1394456103 -3600
# Node ID d74fed45fa8b31eb5c63999282be392039677334
# Parent  0921c1dc344c9ebb83bbdaa31a65d10c693b7edf
abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;

diff -r 0921c1dc344c -r d74fed45fa8b src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -32,11 +32,11 @@
 
 fun consts_of thy =
  let
-   val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
-   val consts = Symtab.dest const_table
+   val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
+   val consts = Symtab.dest constants
  in
    map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
-     (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
+     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) consts)
  end;
 
 
diff -r 0921c1dc344c -r d74fed45fa8b src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -230,7 +230,7 @@
     [Pretty.block
       (Pretty.breaks
         (Pretty.str "(co)inductives:" ::
-          map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
+          map (Pretty.mark_str o #1) (Name_Space.extern_table' ctxt space infos))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
   end |> Pretty.chunks |> Pretty.writeln;
 
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -54,17 +54,26 @@
   val naming_of: Context.generic -> naming
   val map_naming: (naming -> naming) -> Context.generic -> Context.generic
   val declare: Context.generic -> bool -> binding -> T -> string * T
-  type 'a table = T * 'a Symtab.table
+  type 'a table
+  val space_of_table: 'a table -> T
   val check_reports: Context.generic -> 'a table ->
     xstring * Position.T list -> (string * Position.report list) * 'a
   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
+  val lookup_key: 'a table -> string -> (string * 'a) option
   val get: 'a table -> string -> 'a
   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
+  val alias_table: naming -> binding -> string -> 'a table -> 'a table
+  val hide_table: bool -> string -> 'a table -> 'a table
+  val del_table: string -> 'a table -> 'a table
+  val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
+  val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
   val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
     'a table * 'a table -> 'a table
-  val dest_table: Proof.context -> 'a table -> (string * 'a) list
+  val dest_table': Proof.context -> T -> 'a Symtab.table -> ((string * xstring) * 'a) list
+  val dest_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
+  val extern_table': Proof.context -> T -> 'a Symtab.table -> ((Markup.T * xstring) * 'a) list
   val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
 end;
 
@@ -455,9 +464,11 @@
 
 (* definition in symbol table *)
 
-type 'a table = T * 'a Symtab.table;
+datatype 'a table = Table of T * 'a Symtab.table;
 
-fun check_reports context (space, tab) (xname, ps) =
+fun space_of_table (Table (space, _)) = space;
+
+fun check_reports context (Table (space, tab)) (xname, ps) =
   let val name = intern space xname in
     (case Symtab.lookup tab name of
       SOME x =>
@@ -481,31 +492,61 @@
     val _ = Position.reports reports;
   in (name, x) end;
 
-fun get (space, tab) name =
-  (case Symtab.lookup tab name of
-    SOME x => x
-  | NONE => error (undefined (kind_of space) name));
+fun lookup_key (Table (_, tab)) name = Symtab.lookup_key tab name;
+
+fun get table name =
+  (case lookup_key table name of
+    SOME (_, x) => x
+  | NONE => error (undefined (kind_of (space_of_table table)) name));
 
-fun define context strict (binding, x) (space, tab) =
-  let val (name, space') = declare context strict binding space
-  in (name, (space', Symtab.update (name, x) tab)) end;
+fun define context strict (binding, x) (Table (space, tab)) =
+  let
+    val (name, space') = declare context strict binding space;
+    val tab' = Symtab.update (name, x) tab;
+  in (name, Table (space', tab')) end;
+
+
+(* derived table operations *)
+
+fun alias_table naming binding name (Table (space, tab)) =
+  Table (alias naming binding name space, tab);
+
+fun hide_table fully name (Table (space, tab)) =
+  Table (hide fully name space, tab);
 
-fun empty_table kind = (empty kind, Symtab.empty);
+fun del_table name (Table (space, tab)) =
+  let
+    val space' = hide true name space handle ERROR _ => space;
+    val tab' = Symtab.delete_safe name tab;
+  in Table (space', tab') end;
 
-fun merge_tables ((space1, tab1), (space2, tab2)) =
-  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
+fun map_table_entry name f (Table (space, tab)) =
+  Table (space, Symtab.map_entry name f tab);
+
+fun fold_table f (Table (_, tab)) = Symtab.fold f tab;
 
-fun join_tables f ((space1, tab1), (space2, tab2)) =
-  (merge (space1, space2), Symtab.join f (tab1, tab2));
+fun empty_table kind = Table (empty kind, Symtab.empty);
+
+fun merge_tables (Table (space1, tab1), Table (space2, tab2)) =
+  Table (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
 
-fun ext_table ctxt (space, tab) =
+fun join_tables f (Table (space1, tab1), Table (space2, tab2)) =
+  Table (merge (space1, space2), Symtab.join f (tab1, tab2));
+
+
+(* present table content *)
+
+fun dest_table' ctxt space tab =
   Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
   |> Library.sort_wrt (#2 o #1);
 
-fun dest_table ctxt table = map (apfst #1) (ext_table ctxt table);
+fun dest_table ctxt (Table (space, tab)) = dest_table' ctxt space tab;
 
-fun extern_table ctxt (space, tab) =
-  map (fn ((name, xname), x) => ((markup space name, xname), x)) (ext_table ctxt (space, tab));
+fun extern_table' ctxt space tab =
+  dest_table' ctxt space tab
+  |> map (fn ((name, xname), x) => ((markup space name, xname), x));
+
+fun extern_table ctxt (Table (space, tab)) = extern_table' ctxt space tab;
 
 end;
 
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -129,7 +129,8 @@
 
 (* pretty printing *)
 
-fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
+fun extern ctxt =
+  Name_Space.extern ctxt (Name_Space.space_of_table (get_attributes (Context.Proof ctxt)));
 
 fun pretty_attribs _ [] = []
   | pretty_attribs ctxt srcs =
@@ -139,12 +140,12 @@
 (* get attributes *)
 
 fun attribute_generic context =
-  let val (_, tab) = get_attributes context in
+  let val table = get_attributes context in
     fn src =>
       let val ((name, _), pos) = Args.dest_src src in
-        (case Symtab.lookup tab name of
+        (case Name_Space.lookup_key table name of
           NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
-        | SOME (att, _) => att src)
+        | SOME (_, (att, _)) => att src)
       end
   end;
 
@@ -349,8 +350,8 @@
         Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
           Pretty.brk 1, Pretty.str (Config.print_value value)]
       end;
-    val space = #1 (get_attributes (Context.Proof ctxt));
-    val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
+    val space = Name_Space.space_of_table (get_attributes (Context.Proof ctxt));
+    val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
 
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/bundle.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -46,8 +46,8 @@
 val get_bundles = Data.get o Context.Proof;
 
 fun the_bundle ctxt name =
-  (case Symtab.lookup (#2 (get_bundles ctxt)) name of
-    SOME bundle => bundle
+  (case Name_Space.lookup_key (get_bundles ctxt) name of
+    SOME (_, bundle) => bundle
   | NONE => error ("Unknown bundle " ^ quote name));
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -160,19 +160,20 @@
   val merge = Name_Space.join_tables (K merge_locale);
 );
 
-val intern = Name_Space.intern o #1 o Locales.get;
+val locale_space = Name_Space.space_of_table o Locales.get;
+val intern = Name_Space.intern o locale_space;
 fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
 
-fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
+fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy);
 
 fun markup_extern ctxt =
-  Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt)));
+  Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt));
 
 fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
 fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
 
-val get_locale = Symtab.lookup o #2 o Locales.get;
-val defined = Symtab.defined o #2 o Locales.get;
+val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get);
+val defined = is_some oo get_locale;
 
 fun the_locale thy name =
   (case get_locale thy name of
@@ -189,7 +190,7 @@
           (* FIXME Morphism.identity *)
 
 fun change_locale name =
-  Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
+  Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
 
 
 (** Primitive operations **)
@@ -680,6 +681,7 @@
      {name = name,
       parents = map (fst o fst) (dependencies_of thy name),
       body = pretty_locale thy false name};
-  in map make_node (Symtab.keys (#2 (Locales.get thy))) end;
+    val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []);
+  in map make_node names end;
 
 end;
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -351,12 +351,12 @@
 (* get methods *)
 
 fun method ctxt =
-  let val (_, tab) = get_methods ctxt in
+  let val table = get_methods ctxt in
     fn src =>
       let val ((name, _), pos) = Args.dest_src src in
-        (case Symtab.lookup tab name of
+        (case Name_Space.lookup_key table name of
           NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
-        | SOME (meth, _) => meth src)
+        | SOME (_, (meth, _)) => meth src)
       end
   end;
 
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -1152,16 +1152,14 @@
 (** cases **)
 
 fun dest_cases ctxt =
-  Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) []
+  Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
   |> sort (int_ord o pairself #1) |> map #2;
 
 local
 
 fun update_case _ _ ("", _) res = res
-  | update_case _ _ (name, NONE) ((space, tab), index) =
-      let
-        val tab' = Symtab.delete_safe name tab;
-      in ((space, tab'), index) end
+  | update_case _ _ (name, NONE) (cases, index) =
+      (Name_Space.del_table name cases, index)
   | update_case context is_proper (name, SOME c) (cases, index) =
       let
         val (_, cases') = cases |> Name_Space.define context false
@@ -1179,7 +1177,7 @@
   let
     val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming);
     val cases = cases_of ctxt;
-    val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0;
+    val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
     val (cases', _) = fold (update_case context is_proper) args (cases, index);
   in map_cases (K cases') ctxt end;
 
@@ -1230,14 +1228,15 @@
 
 fun pretty_abbrevs show_globals ctxt =
   let
-    val ((space, consts), (_, globals)) =
+    val space = const_space ctxt;
+    val (constants, globals) =
       pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
     fun add_abbr (_, (_, NONE)) = I
       | 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 =
-      Name_Space.extern_table ctxt (space, Symtab.make (Symtab.fold add_abbr consts []));
+      Name_Space.extern_table' ctxt space (Symtab.make (Symtab.fold add_abbr constants []));
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -58,8 +58,8 @@
 fun pretty_const ctxt (c, ty) =
   let
     val ty' = Logic.unvarifyT_global ty;
-    val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
-    val markup = Name_Space.markup consts_space c;
+    val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
+    val markup = Name_Space.markup const_space c;
   in
     Pretty.block
      [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
@@ -103,13 +103,13 @@
     val criteria = map make_criterion raw_criteria;
 
     val consts = Sign.consts_of thy;
-    val (_, consts_tab) = #constants (Consts.dest consts);
+    val {constants, ...} = Consts.dest consts;
     fun eval_entry c =
       fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
 
     val matches =
       Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
-        consts_tab []
+        constants []
       |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
       |> map (apsnd fst o snd);
   in
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/consts.ML
--- a/src/Pure/consts.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/consts.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -11,8 +11,9 @@
   val eq_consts: T * T -> bool
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
-   {constants: (typ * term option) Name_Space.table,
-    constraints: typ Name_Space.table}
+   {const_space: Name_Space.T,
+    constants: (typ * term option) Symtab.table,
+    constraints: typ Symtab.table}
   val the_const: T -> string -> string * typ                   (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
@@ -80,17 +81,18 @@
 
 (* dest consts *)
 
-fun dest (Consts {decls = (space, decls), constraints, ...}) =
- {constants = (space,
-    Symtab.fold (fn (c, ({T, ...}, abbr)) =>
-      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
-  constraints = (space, constraints)};
+fun dest (Consts {decls, constraints, ...}) =
+ {const_space = Name_Space.space_of_table decls,
+  constants =
+    Name_Space.fold_table (fn (c, ({T, ...}, abbr)) =>
+      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty,
+  constraints = constraints};
 
 
 (* lookup consts *)
 
-fun the_entry (Consts {decls = (_, tab), ...}) c =
-  (case Symtab.lookup_key tab c of
+fun the_entry (Consts {decls, ...}) c =
+  (case Name_Space.lookup_key decls c of
     SOME entry => entry
   | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
 
@@ -118,10 +120,10 @@
 
 (* name space and syntax *)
 
-fun space_of (Consts {decls = (space, _), ...}) = space;
+fun space_of (Consts {decls, ...}) = Name_Space.space_of_table decls;
 
-fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) =>
-  ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs));
+fun alias naming binding name = map_consts (fn (decls, constraints, rev_abbrevs) =>
+  ((Name_Space.alias_table naming binding name decls), constraints, rev_abbrevs));
 
 val is_concealed = Name_Space.is_concealed o space_of;
 
@@ -219,7 +221,7 @@
 (* name space *)
 
 fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
-  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
+  (Name_Space.hide_table fully c decls, constraints, rev_abbrevs));
 
 
 (* declarations *)
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/display.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -145,33 +145,34 @@
     fun pretty_restrict (const, name) =
       Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
 
-    val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
     val tsig = Sign.tsig_of thy;
     val consts = Sign.consts_of thy;
-    val {constants, constraints} = Consts.dest consts;
-    val extern_const = Name_Space.extern ctxt (#1 constants);
+    val {const_space, constants, constraints} = Consts.dest consts;
+    val extern_const = Name_Space.extern ctxt const_space;
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
-      Name_Space.dest_table ctxt (class_space,
-        Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)));
-    val tdecls = Name_Space.dest_table ctxt types;
-    val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
+      Name_Space.dest_table' ctxt class_space
+        (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)))
+      |> map (apfst #1);
+    val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1);
+    val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1);
 
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-    val cnsts = Name_Space.extern_table ctxt (#1 constants,
-      Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
+    val cnsts =
+      Name_Space.extern_table' ctxt const_space
+        (Symtab.make (filter_out (prune_const o fst) (Symtab.dest 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 = Name_Space.extern_table ctxt constraints;
+    val cnstrs = Name_Space.extern_table' ctxt const_space constraints;
 
-    val axms = Name_Space.extern_table ctxt axioms;
+    val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy);
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/facts.ML
--- a/src/Pure/facts.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/facts.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -140,8 +140,7 @@
 
 fun facts_of (Facts {facts, ...}) = facts;
 
-val space_of = #1 o facts_of;
-val table_of = #2 o facts_of;
+val space_of = Name_Space.space_of_table o facts_of;
 
 val is_concealed = Name_Space.is_concealed o space_of;
 
@@ -157,16 +156,16 @@
 val intern = Name_Space.intern o space_of;
 fun extern ctxt = Name_Space.extern ctxt o space_of;
 
-val defined = Symtab.defined o table_of;
+val defined = is_some oo (Name_Space.lookup_key o facts_of);
 
 fun lookup context facts name =
-  (case Symtab.lookup (table_of facts) name of
+  (case Name_Space.lookup_key (facts_of facts) name of
     NONE => NONE
-  | SOME (Static ths) => SOME (true, ths)
-  | SOME (Dynamic f) => SOME (false, f context));
+  | SOME (_, Static ths) => SOME (true, ths)
+  | SOME (_, Dynamic f) => SOME (false, f context));
 
 fun fold_static f =
-  Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
+  Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
 
 
 (* content difference *)
@@ -221,13 +220,10 @@
 
 (* remove entries *)
 
-fun del name (Facts {facts = (space, tab), props}) =
-  let
-    val space' = Name_Space.hide true name space handle ERROR _ => space;
-    val tab' = Symtab.delete_safe name tab;
-  in make_facts (space', tab') props end;
+fun del name (Facts {facts, props}) =
+  make_facts (Name_Space.del_table name facts) props;
 
-fun hide fully name (Facts {facts = (space, tab), props}) =
-  make_facts (Name_Space.hide fully name space, tab) props;
+fun hide fully name (Facts {facts, props}) =
+  make_facts (Name_Space.hide_table fully name facts) props;
 
 end;
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/sign.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -192,7 +192,7 @@
 
 fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
 
-val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
+val declared_tyname = is_some oo (Name_Space.lookup_key o #types o Type.rep_tsig o tsig_of);
 val declared_const = can o the_const_constraint;
 
 
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/term_sharing.ML
--- a/src/Pure/term_sharing.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/term_sharing.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -19,10 +19,10 @@
 
 fun init thy =
   let
-    val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
+    val {classes = (_, algebra), types, ...} = Type.rep_tsig (Sign.tsig_of thy);
 
     val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
-    val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
+    val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types);
     val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
 
     val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/theory.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -17,8 +17,8 @@
   val requires: theory -> string -> string -> unit
   val setup: (theory -> theory) -> unit
   val get_markup: theory -> Markup.T
+  val axiom_table: theory -> term Name_Space.table
   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
   val defs_of: theory -> Defs.T
@@ -139,10 +139,10 @@
 
 (* basic operations *)
 
-val axiom_space = #1 o #axioms o rep_theory;
-val axiom_table = #2 o #axioms o rep_theory;
+val axiom_table = #axioms o rep_theory;
+val axiom_space = Name_Space.space_of_table o axiom_table;
 
-val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
+fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []);
 fun all_axioms_of thy = maps axioms_of (nodes_of thy);
 
 val defs_of = #defs o rep_theory;
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/thm.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -584,8 +584,8 @@
 fun axiom theory name =
   let
     fun get_ax thy =
-      Symtab.lookup (Theory.axiom_table thy) name
-      |> Option.map (fn prop =>
+      Name_Space.lookup_key (Theory.axiom_table thy) name
+      |> Option.map (fn (_, prop) =>
            let
              val der = deriv_rule0 (Proofterm.axm_proof name prop);
              val maxidx = maxidx_of_term prop;
@@ -602,7 +602,7 @@
 
 (*return additional axioms of this theory node*)
 fun axioms_of thy =
-  map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
+  map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy);
 
 
 (* tags *)
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/type.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -177,7 +177,7 @@
 fun build_tsig (classes, default, types) =
   let
     val log_types =
-      Symtab.fold (fn (c, LogicalType n) => cons (c, n) | _ => I) (snd types) []
+      Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types []
       |> Library.sort (int_ord o pairself snd) |> map fst;
   in make_tsig (classes, default, types, log_types) end;
 
@@ -237,17 +237,17 @@
 
 (* types *)
 
-val type_space = #1 o #types o rep_tsig;
+val type_space = Name_Space.space_of_table o #types o rep_tsig;
 
-fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
-  (classes, default, (Name_Space.alias naming binding name space, types)));
+fun type_alias naming binding name = map_tsig (fn (classes, default, types) =>
+  (classes, default, (Name_Space.alias_table naming binding name types)));
 
 val is_logtype = member (op =) o logical_types;
 
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
-fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
+fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
 
 fun check_decl context (TSig {types, ...}) (c, pos) =
   Name_Space.check_reports context types (c, [pos]);
@@ -639,14 +639,15 @@
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
-    val (space', tab') = f types;
-    val _ = Name_Space.intern space' "dummy" = "dummy" orelse
-      error "Illegal declaration of dummy type";
-  in (classes, default, (space', tab')) end);
+    val types' = f types;
+    val _ =
+      Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
+        error "Illegal declaration of dummy type";
+  in (classes, default, types') end);
 
-fun syntactic types (Type (c, Ts)) =
-      (case Symtab.lookup types c of SOME Nonterminal => true | _ => false)
-        orelse exists (syntactic types) Ts
+fun syntactic tsig (Type (c, Ts)) =
+      (case lookup_type tsig c of SOME Nonterminal => true | _ => false)
+        orelse exists (syntactic tsig) Ts
   | syntactic _ _ = false;
 
 in
@@ -669,14 +670,14 @@
       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
         [] => []
       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
-  in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
+  in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic tsig rhs')) end);
 
 fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal;
 
 end;
 
-fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
-  (classes, default, (Name_Space.hide fully c space, types)));
+fun hide_type fully c = map_tsig (fn (classes, default, types) =>
+  (classes, default, Name_Space.hide_table fully c types));
 
 
 (* merge type signatures *)
diff -r 0921c1dc344c -r d74fed45fa8b src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Pure/variable.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -175,7 +175,7 @@
 
 val names_of = #names o rep_data;
 val fixes_of = #fixes o rep_data;
-val fixes_space = #1 o fixes_of;
+val fixes_space = Name_Space.space_of_table o fixes_of;
 val binds_of = #binds o rep_data;
 val type_occs_of = #type_occs o rep_data;
 val maxidx_of = #maxidx o rep_data;
@@ -342,8 +342,8 @@
   in if is_fixed ctxt x' then SOME x' else NONE end;
 
 fun revert_fixed ctxt x =
-  (case Symtab.lookup (#2 (fixes_of ctxt)) x of
-    SOME x' => if intern_fixed ctxt x' = x then x' else x
+  (case Name_Space.lookup_key (fixes_of ctxt) x of
+    SOME (_, x') => if intern_fixed ctxt x' = x then x' else x
   | NONE => x);
 
 fun markup_fixed ctxt x =
@@ -351,8 +351,8 @@
   |> Markup.name (revert_fixed ctxt x);
 
 fun dest_fixes ctxt =
-  let val (space, tab) = fixes_of ctxt
-  in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
+  Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) []
+  |> sort (Name_Space.entry_ord (fixes_space ctxt) o pairself #2);
 
 
 (* collect variables *)
@@ -383,8 +383,8 @@
     let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
       ctxt
       |> map_fixes
-        (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>>
-          Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
+        (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>
+          Name_Space.alias_table Name_Space.default_naming (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;
@@ -450,8 +450,8 @@
     val still_fixed = not o newly_fixed inner outer;
 
     val gen_fixes =
-      Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
-        (#2 (fixes_of inner)) [];
+      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)
+        (fixes_of inner) [];
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
diff -r 0921c1dc344c -r d74fed45fa8b src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Mar 10 10:13:47 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Mar 10 13:55:03 2014 +0100
@@ -877,7 +877,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
-      ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
+      (#constants (Consts.dest (Sign.consts_of thy'))) [];
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');