abstract type Name_Space.table;
authorwenzelm
Mon Mar 10 13:55:03 2014 +0100 (2014-03-10)
changeset 56025d74fed45fa8b
parent 56024 0921c1dc344c
child 56026 893fe12639bc
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;
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Tools/inductive.ML
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/bundle.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/Tools/find_consts.ML
src/Pure/consts.ML
src/Pure/display.ML
src/Pure/facts.ML
src/Pure/sign.ML
src/Pure/term_sharing.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/variable.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Mon Mar 10 10:13:47 2014 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Mar 10 13:55:03 2014 +0100
     1.3 @@ -32,11 +32,11 @@
     1.4  
     1.5  fun consts_of thy =
     1.6   let
     1.7 -   val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
     1.8 -   val consts = Symtab.dest const_table
     1.9 +   val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
    1.10 +   val consts = Symtab.dest constants
    1.11   in
    1.12     map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
    1.13 -     (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
    1.14 +     (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) consts)
    1.15   end;
    1.16  
    1.17  
     2.1 --- a/src/HOL/Tools/inductive.ML	Mon Mar 10 10:13:47 2014 +0100
     2.2 +++ b/src/HOL/Tools/inductive.ML	Mon Mar 10 13:55:03 2014 +0100
     2.3 @@ -230,7 +230,7 @@
     2.4      [Pretty.block
     2.5        (Pretty.breaks
     2.6          (Pretty.str "(co)inductives:" ::
     2.7 -          map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
     2.8 +          map (Pretty.mark_str o #1) (Name_Space.extern_table' ctxt space infos))),
     2.9       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
    2.10    end |> Pretty.chunks |> Pretty.writeln;
    2.11  
     3.1 --- a/src/Pure/General/name_space.ML	Mon Mar 10 10:13:47 2014 +0100
     3.2 +++ b/src/Pure/General/name_space.ML	Mon Mar 10 13:55:03 2014 +0100
     3.3 @@ -54,17 +54,26 @@
     3.4    val naming_of: Context.generic -> naming
     3.5    val map_naming: (naming -> naming) -> Context.generic -> Context.generic
     3.6    val declare: Context.generic -> bool -> binding -> T -> string * T
     3.7 -  type 'a table = T * 'a Symtab.table
     3.8 +  type 'a table
     3.9 +  val space_of_table: 'a table -> T
    3.10    val check_reports: Context.generic -> 'a table ->
    3.11      xstring * Position.T list -> (string * Position.report list) * 'a
    3.12    val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    3.13 +  val lookup_key: 'a table -> string -> (string * 'a) option
    3.14    val get: 'a table -> string -> 'a
    3.15    val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    3.16 +  val alias_table: naming -> binding -> string -> 'a table -> 'a table
    3.17 +  val hide_table: bool -> string -> 'a table -> 'a table
    3.18 +  val del_table: string -> 'a table -> 'a table
    3.19 +  val map_table_entry: string -> ('a -> 'a) -> 'a table -> 'a table
    3.20 +  val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
    3.21    val empty_table: string -> 'a table
    3.22    val merge_tables: 'a table * 'a table -> 'a table
    3.23    val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
    3.24      'a table * 'a table -> 'a table
    3.25 -  val dest_table: Proof.context -> 'a table -> (string * 'a) list
    3.26 +  val dest_table': Proof.context -> T -> 'a Symtab.table -> ((string * xstring) * 'a) list
    3.27 +  val dest_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
    3.28 +  val extern_table': Proof.context -> T -> 'a Symtab.table -> ((Markup.T * xstring) * 'a) list
    3.29    val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
    3.30  end;
    3.31  
    3.32 @@ -455,9 +464,11 @@
    3.33  
    3.34  (* definition in symbol table *)
    3.35  
    3.36 -type 'a table = T * 'a Symtab.table;
    3.37 +datatype 'a table = Table of T * 'a Symtab.table;
    3.38  
    3.39 -fun check_reports context (space, tab) (xname, ps) =
    3.40 +fun space_of_table (Table (space, _)) = space;
    3.41 +
    3.42 +fun check_reports context (Table (space, tab)) (xname, ps) =
    3.43    let val name = intern space xname in
    3.44      (case Symtab.lookup tab name of
    3.45        SOME x =>
    3.46 @@ -481,31 +492,61 @@
    3.47      val _ = Position.reports reports;
    3.48    in (name, x) end;
    3.49  
    3.50 -fun get (space, tab) name =
    3.51 -  (case Symtab.lookup tab name of
    3.52 -    SOME x => x
    3.53 -  | NONE => error (undefined (kind_of space) name));
    3.54 +fun lookup_key (Table (_, tab)) name = Symtab.lookup_key tab name;
    3.55 +
    3.56 +fun get table name =
    3.57 +  (case lookup_key table name of
    3.58 +    SOME (_, x) => x
    3.59 +  | NONE => error (undefined (kind_of (space_of_table table)) name));
    3.60  
    3.61 -fun define context strict (binding, x) (space, tab) =
    3.62 -  let val (name, space') = declare context strict binding space
    3.63 -  in (name, (space', Symtab.update (name, x) tab)) end;
    3.64 +fun define context strict (binding, x) (Table (space, tab)) =
    3.65 +  let
    3.66 +    val (name, space') = declare context strict binding space;
    3.67 +    val tab' = Symtab.update (name, x) tab;
    3.68 +  in (name, Table (space', tab')) end;
    3.69 +
    3.70 +
    3.71 +(* derived table operations *)
    3.72 +
    3.73 +fun alias_table naming binding name (Table (space, tab)) =
    3.74 +  Table (alias naming binding name space, tab);
    3.75 +
    3.76 +fun hide_table fully name (Table (space, tab)) =
    3.77 +  Table (hide fully name space, tab);
    3.78  
    3.79 -fun empty_table kind = (empty kind, Symtab.empty);
    3.80 +fun del_table name (Table (space, tab)) =
    3.81 +  let
    3.82 +    val space' = hide true name space handle ERROR _ => space;
    3.83 +    val tab' = Symtab.delete_safe name tab;
    3.84 +  in Table (space', tab') end;
    3.85  
    3.86 -fun merge_tables ((space1, tab1), (space2, tab2)) =
    3.87 -  (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
    3.88 +fun map_table_entry name f (Table (space, tab)) =
    3.89 +  Table (space, Symtab.map_entry name f tab);
    3.90 +
    3.91 +fun fold_table f (Table (_, tab)) = Symtab.fold f tab;
    3.92  
    3.93 -fun join_tables f ((space1, tab1), (space2, tab2)) =
    3.94 -  (merge (space1, space2), Symtab.join f (tab1, tab2));
    3.95 +fun empty_table kind = Table (empty kind, Symtab.empty);
    3.96 +
    3.97 +fun merge_tables (Table (space1, tab1), Table (space2, tab2)) =
    3.98 +  Table (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
    3.99  
   3.100 -fun ext_table ctxt (space, tab) =
   3.101 +fun join_tables f (Table (space1, tab1), Table (space2, tab2)) =
   3.102 +  Table (merge (space1, space2), Symtab.join f (tab1, tab2));
   3.103 +
   3.104 +
   3.105 +(* present table content *)
   3.106 +
   3.107 +fun dest_table' ctxt space tab =
   3.108    Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
   3.109    |> Library.sort_wrt (#2 o #1);
   3.110  
   3.111 -fun dest_table ctxt table = map (apfst #1) (ext_table ctxt table);
   3.112 +fun dest_table ctxt (Table (space, tab)) = dest_table' ctxt space tab;
   3.113  
   3.114 -fun extern_table ctxt (space, tab) =
   3.115 -  map (fn ((name, xname), x) => ((markup space name, xname), x)) (ext_table ctxt (space, tab));
   3.116 +fun extern_table' ctxt space tab =
   3.117 +  dest_table' ctxt space tab
   3.118 +  |> map (fn ((name, xname), x) => ((markup space name, xname), x));
   3.119 +
   3.120 +fun extern_table ctxt (Table (space, tab)) = extern_table' ctxt space tab;
   3.121  
   3.122  end;
   3.123  
     4.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 10 10:13:47 2014 +0100
     4.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 13:55:03 2014 +0100
     4.3 @@ -129,7 +129,8 @@
     4.4  
     4.5  (* pretty printing *)
     4.6  
     4.7 -fun extern ctxt = Name_Space.extern ctxt (#1 (get_attributes (Context.Proof ctxt)));
     4.8 +fun extern ctxt =
     4.9 +  Name_Space.extern ctxt (Name_Space.space_of_table (get_attributes (Context.Proof ctxt)));
    4.10  
    4.11  fun pretty_attribs _ [] = []
    4.12    | pretty_attribs ctxt srcs =
    4.13 @@ -139,12 +140,12 @@
    4.14  (* get attributes *)
    4.15  
    4.16  fun attribute_generic context =
    4.17 -  let val (_, tab) = get_attributes context in
    4.18 +  let val table = get_attributes context in
    4.19      fn src =>
    4.20        let val ((name, _), pos) = Args.dest_src src in
    4.21 -        (case Symtab.lookup tab name of
    4.22 +        (case Name_Space.lookup_key table name of
    4.23            NONE => error ("Undefined attribute: " ^ quote name ^ Position.here pos)
    4.24 -        | SOME (att, _) => att src)
    4.25 +        | SOME (_, (att, _)) => att src)
    4.26        end
    4.27    end;
    4.28  
    4.29 @@ -349,8 +350,8 @@
    4.30          Pretty.block [Pretty.mark_str name, Pretty.str (": " ^ Config.print_type value ^ " ="),
    4.31            Pretty.brk 1, Pretty.str (Config.print_value value)]
    4.32        end;
    4.33 -    val space = #1 (get_attributes (Context.Proof ctxt));
    4.34 -    val configs = Name_Space.extern_table ctxt (space, Configs.get (Proof_Context.theory_of ctxt));
    4.35 +    val space = Name_Space.space_of_table (get_attributes (Context.Proof ctxt));
    4.36 +    val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
    4.37    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
    4.38  
    4.39  
     5.1 --- a/src/Pure/Isar/bundle.ML	Mon Mar 10 10:13:47 2014 +0100
     5.2 +++ b/src/Pure/Isar/bundle.ML	Mon Mar 10 13:55:03 2014 +0100
     5.3 @@ -46,8 +46,8 @@
     5.4  val get_bundles = Data.get o Context.Proof;
     5.5  
     5.6  fun the_bundle ctxt name =
     5.7 -  (case Symtab.lookup (#2 (get_bundles ctxt)) name of
     5.8 -    SOME bundle => bundle
     5.9 +  (case Name_Space.lookup_key (get_bundles ctxt) name of
    5.10 +    SOME (_, bundle) => bundle
    5.11    | NONE => error ("Unknown bundle " ^ quote name));
    5.12  
    5.13  fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
     6.1 --- a/src/Pure/Isar/locale.ML	Mon Mar 10 10:13:47 2014 +0100
     6.2 +++ b/src/Pure/Isar/locale.ML	Mon Mar 10 13:55:03 2014 +0100
     6.3 @@ -160,19 +160,20 @@
     6.4    val merge = Name_Space.join_tables (K merge_locale);
     6.5  );
     6.6  
     6.7 -val intern = Name_Space.intern o #1 o Locales.get;
     6.8 +val locale_space = Name_Space.space_of_table o Locales.get;
     6.9 +val intern = Name_Space.intern o locale_space;
    6.10  fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
    6.11  
    6.12 -fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
    6.13 +fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy);
    6.14  
    6.15  fun markup_extern ctxt =
    6.16 -  Name_Space.markup_extern ctxt (#1 (Locales.get (Proof_Context.theory_of ctxt)));
    6.17 +  Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt));
    6.18  
    6.19  fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
    6.20  fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
    6.21  
    6.22 -val get_locale = Symtab.lookup o #2 o Locales.get;
    6.23 -val defined = Symtab.defined o #2 o Locales.get;
    6.24 +val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get);
    6.25 +val defined = is_some oo get_locale;
    6.26  
    6.27  fun the_locale thy name =
    6.28    (case get_locale thy name of
    6.29 @@ -189,7 +190,7 @@
    6.30            (* FIXME Morphism.identity *)
    6.31  
    6.32  fun change_locale name =
    6.33 -  Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
    6.34 +  Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
    6.35  
    6.36  
    6.37  (** Primitive operations **)
    6.38 @@ -680,6 +681,7 @@
    6.39       {name = name,
    6.40        parents = map (fst o fst) (dependencies_of thy name),
    6.41        body = pretty_locale thy false name};
    6.42 -  in map make_node (Symtab.keys (#2 (Locales.get thy))) end;
    6.43 +    val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []);
    6.44 +  in map make_node names end;
    6.45  
    6.46  end;
     7.1 --- a/src/Pure/Isar/method.ML	Mon Mar 10 10:13:47 2014 +0100
     7.2 +++ b/src/Pure/Isar/method.ML	Mon Mar 10 13:55:03 2014 +0100
     7.3 @@ -351,12 +351,12 @@
     7.4  (* get methods *)
     7.5  
     7.6  fun method ctxt =
     7.7 -  let val (_, tab) = get_methods ctxt in
     7.8 +  let val table = get_methods ctxt in
     7.9      fn src =>
    7.10        let val ((name, _), pos) = Args.dest_src src in
    7.11 -        (case Symtab.lookup tab name of
    7.12 +        (case Name_Space.lookup_key table name of
    7.13            NONE => error ("Undefined method: " ^ quote name ^ Position.here pos)
    7.14 -        | SOME (meth, _) => meth src)
    7.15 +        | SOME (_, (meth, _)) => meth src)
    7.16        end
    7.17    end;
    7.18  
     8.1 --- a/src/Pure/Isar/proof_context.ML	Mon Mar 10 10:13:47 2014 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Mar 10 13:55:03 2014 +0100
     8.3 @@ -1152,16 +1152,14 @@
     8.4  (** cases **)
     8.5  
     8.6  fun dest_cases ctxt =
     8.7 -  Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) []
     8.8 +  Name_Space.fold_table (fn (a, (c, i)) => cons (i, (a, c))) (cases_of ctxt) []
     8.9    |> sort (int_ord o pairself #1) |> map #2;
    8.10  
    8.11  local
    8.12  
    8.13  fun update_case _ _ ("", _) res = res
    8.14 -  | update_case _ _ (name, NONE) ((space, tab), index) =
    8.15 -      let
    8.16 -        val tab' = Symtab.delete_safe name tab;
    8.17 -      in ((space, tab'), index) end
    8.18 +  | update_case _ _ (name, NONE) (cases, index) =
    8.19 +      (Name_Space.del_table name cases, index)
    8.20    | update_case context is_proper (name, SOME c) (cases, index) =
    8.21        let
    8.22          val (_, cases') = cases |> Name_Space.define context false
    8.23 @@ -1179,7 +1177,7 @@
    8.24    let
    8.25      val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming);
    8.26      val cases = cases_of ctxt;
    8.27 -    val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0;
    8.28 +    val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
    8.29      val (cases', _) = fold (update_case context is_proper) args (cases, index);
    8.30    in map_cases (K cases') ctxt end;
    8.31  
    8.32 @@ -1230,14 +1228,15 @@
    8.33  
    8.34  fun pretty_abbrevs show_globals ctxt =
    8.35    let
    8.36 -    val ((space, consts), (_, globals)) =
    8.37 +    val space = const_space ctxt;
    8.38 +    val (constants, globals) =
    8.39        pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
    8.40      fun add_abbr (_, (_, NONE)) = I
    8.41        | add_abbr (c, (T, SOME t)) =
    8.42            if not show_globals andalso Symtab.defined globals c then I
    8.43            else cons (c, Logic.mk_equals (Const (c, T), t));
    8.44      val abbrevs =
    8.45 -      Name_Space.extern_table ctxt (space, Symtab.make (Symtab.fold add_abbr consts []));
    8.46 +      Name_Space.extern_table' ctxt space (Symtab.make (Symtab.fold add_abbr constants []));
    8.47    in
    8.48      if null abbrevs then []
    8.49      else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
     9.1 --- a/src/Pure/Tools/find_consts.ML	Mon Mar 10 10:13:47 2014 +0100
     9.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Mar 10 13:55:03 2014 +0100
     9.3 @@ -58,8 +58,8 @@
     9.4  fun pretty_const ctxt (c, ty) =
     9.5    let
     9.6      val ty' = Logic.unvarifyT_global ty;
     9.7 -    val consts_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
     9.8 -    val markup = Name_Space.markup consts_space c;
     9.9 +    val const_space = Consts.space_of (Sign.consts_of (Proof_Context.theory_of ctxt));
    9.10 +    val markup = Name_Space.markup const_space c;
    9.11    in
    9.12      Pretty.block
    9.13       [Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1,
    9.14 @@ -103,13 +103,13 @@
    9.15      val criteria = map make_criterion raw_criteria;
    9.16  
    9.17      val consts = Sign.consts_of thy;
    9.18 -    val (_, consts_tab) = #constants (Consts.dest consts);
    9.19 +    val {constants, ...} = Consts.dest consts;
    9.20      fun eval_entry c =
    9.21        fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
    9.22  
    9.23      val matches =
    9.24        Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
    9.25 -        consts_tab []
    9.26 +        constants []
    9.27        |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
    9.28        |> map (apsnd fst o snd);
    9.29    in
    10.1 --- a/src/Pure/consts.ML	Mon Mar 10 10:13:47 2014 +0100
    10.2 +++ b/src/Pure/consts.ML	Mon Mar 10 13:55:03 2014 +0100
    10.3 @@ -11,8 +11,9 @@
    10.4    val eq_consts: T * T -> bool
    10.5    val retrieve_abbrevs: T -> string list -> term -> (term * term) list
    10.6    val dest: T ->
    10.7 -   {constants: (typ * term option) Name_Space.table,
    10.8 -    constraints: typ Name_Space.table}
    10.9 +   {const_space: Name_Space.T,
   10.10 +    constants: (typ * term option) Symtab.table,
   10.11 +    constraints: typ Symtab.table}
   10.12    val the_const: T -> string -> string * typ                   (*exception TYPE*)
   10.13    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   10.14    val type_scheme: T -> string -> typ                          (*exception TYPE*)
   10.15 @@ -80,17 +81,18 @@
   10.16  
   10.17  (* dest consts *)
   10.18  
   10.19 -fun dest (Consts {decls = (space, decls), constraints, ...}) =
   10.20 - {constants = (space,
   10.21 -    Symtab.fold (fn (c, ({T, ...}, abbr)) =>
   10.22 -      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty),
   10.23 -  constraints = (space, constraints)};
   10.24 +fun dest (Consts {decls, constraints, ...}) =
   10.25 + {const_space = Name_Space.space_of_table decls,
   10.26 +  constants =
   10.27 +    Name_Space.fold_table (fn (c, ({T, ...}, abbr)) =>
   10.28 +      Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty,
   10.29 +  constraints = constraints};
   10.30  
   10.31  
   10.32  (* lookup consts *)
   10.33  
   10.34 -fun the_entry (Consts {decls = (_, tab), ...}) c =
   10.35 -  (case Symtab.lookup_key tab c of
   10.36 +fun the_entry (Consts {decls, ...}) c =
   10.37 +  (case Name_Space.lookup_key decls c of
   10.38      SOME entry => entry
   10.39    | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
   10.40  
   10.41 @@ -118,10 +120,10 @@
   10.42  
   10.43  (* name space and syntax *)
   10.44  
   10.45 -fun space_of (Consts {decls = (space, _), ...}) = space;
   10.46 +fun space_of (Consts {decls, ...}) = Name_Space.space_of_table decls;
   10.47  
   10.48 -fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) =>
   10.49 -  ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs));
   10.50 +fun alias naming binding name = map_consts (fn (decls, constraints, rev_abbrevs) =>
   10.51 +  ((Name_Space.alias_table naming binding name decls), constraints, rev_abbrevs));
   10.52  
   10.53  val is_concealed = Name_Space.is_concealed o space_of;
   10.54  
   10.55 @@ -219,7 +221,7 @@
   10.56  (* name space *)
   10.57  
   10.58  fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
   10.59 -  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
   10.60 +  (Name_Space.hide_table fully c decls, constraints, rev_abbrevs));
   10.61  
   10.62  
   10.63  (* declarations *)
    11.1 --- a/src/Pure/display.ML	Mon Mar 10 10:13:47 2014 +0100
    11.2 +++ b/src/Pure/display.ML	Mon Mar 10 13:55:03 2014 +0100
    11.3 @@ -145,33 +145,34 @@
    11.4      fun pretty_restrict (const, name) =
    11.5        Pretty.block ([prt_const' const, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
    11.6  
    11.7 -    val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
    11.8      val defs = Theory.defs_of thy;
    11.9      val {restricts, reducts} = Defs.dest defs;
   11.10      val tsig = Sign.tsig_of thy;
   11.11      val consts = Sign.consts_of thy;
   11.12 -    val {constants, constraints} = Consts.dest consts;
   11.13 -    val extern_const = Name_Space.extern ctxt (#1 constants);
   11.14 +    val {const_space, constants, constraints} = Consts.dest consts;
   11.15 +    val extern_const = Name_Space.extern ctxt const_space;
   11.16      val {classes, default, types, ...} = Type.rep_tsig tsig;
   11.17      val (class_space, class_algebra) = classes;
   11.18      val classes = Sorts.classes_of class_algebra;
   11.19      val arities = Sorts.arities_of class_algebra;
   11.20  
   11.21      val clsses =
   11.22 -      Name_Space.dest_table ctxt (class_space,
   11.23 -        Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)));
   11.24 -    val tdecls = Name_Space.dest_table ctxt types;
   11.25 -    val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
   11.26 +      Name_Space.dest_table' ctxt class_space
   11.27 +        (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)))
   11.28 +      |> map (apfst #1);
   11.29 +    val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1);
   11.30 +    val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1);
   11.31  
   11.32      fun prune_const c = not verbose andalso Consts.is_concealed consts c;
   11.33 -    val cnsts = Name_Space.extern_table ctxt (#1 constants,
   11.34 -      Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
   11.35 +    val cnsts =
   11.36 +      Name_Space.extern_table' ctxt const_space
   11.37 +        (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants)));
   11.38  
   11.39      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   11.40      val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   11.41 -    val cnstrs = Name_Space.extern_table ctxt constraints;
   11.42 +    val cnstrs = Name_Space.extern_table' ctxt const_space constraints;
   11.43  
   11.44 -    val axms = Name_Space.extern_table ctxt axioms;
   11.45 +    val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy);
   11.46  
   11.47      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   11.48        |> map (fn (lhs, rhs) =>
    12.1 --- a/src/Pure/facts.ML	Mon Mar 10 10:13:47 2014 +0100
    12.2 +++ b/src/Pure/facts.ML	Mon Mar 10 13:55:03 2014 +0100
    12.3 @@ -140,8 +140,7 @@
    12.4  
    12.5  fun facts_of (Facts {facts, ...}) = facts;
    12.6  
    12.7 -val space_of = #1 o facts_of;
    12.8 -val table_of = #2 o facts_of;
    12.9 +val space_of = Name_Space.space_of_table o facts_of;
   12.10  
   12.11  val is_concealed = Name_Space.is_concealed o space_of;
   12.12  
   12.13 @@ -157,16 +156,16 @@
   12.14  val intern = Name_Space.intern o space_of;
   12.15  fun extern ctxt = Name_Space.extern ctxt o space_of;
   12.16  
   12.17 -val defined = Symtab.defined o table_of;
   12.18 +val defined = is_some oo (Name_Space.lookup_key o facts_of);
   12.19  
   12.20  fun lookup context facts name =
   12.21 -  (case Symtab.lookup (table_of facts) name of
   12.22 +  (case Name_Space.lookup_key (facts_of facts) name of
   12.23      NONE => NONE
   12.24 -  | SOME (Static ths) => SOME (true, ths)
   12.25 -  | SOME (Dynamic f) => SOME (false, f context));
   12.26 +  | SOME (_, Static ths) => SOME (true, ths)
   12.27 +  | SOME (_, Dynamic f) => SOME (false, f context));
   12.28  
   12.29  fun fold_static f =
   12.30 -  Symtab.fold (fn (name, Static ths) => f (name, ths) | _ => I) o table_of;
   12.31 +  Name_Space.fold_table (fn (name, Static ths) => f (name, ths) | _ => I) o facts_of;
   12.32  
   12.33  
   12.34  (* content difference *)
   12.35 @@ -221,13 +220,10 @@
   12.36  
   12.37  (* remove entries *)
   12.38  
   12.39 -fun del name (Facts {facts = (space, tab), props}) =
   12.40 -  let
   12.41 -    val space' = Name_Space.hide true name space handle ERROR _ => space;
   12.42 -    val tab' = Symtab.delete_safe name tab;
   12.43 -  in make_facts (space', tab') props end;
   12.44 +fun del name (Facts {facts, props}) =
   12.45 +  make_facts (Name_Space.del_table name facts) props;
   12.46  
   12.47 -fun hide fully name (Facts {facts = (space, tab), props}) =
   12.48 -  make_facts (Name_Space.hide fully name space, tab) props;
   12.49 +fun hide fully name (Facts {facts, props}) =
   12.50 +  make_facts (Name_Space.hide_table fully name facts) props;
   12.51  
   12.52  end;
    13.1 --- a/src/Pure/sign.ML	Mon Mar 10 10:13:47 2014 +0100
    13.2 +++ b/src/Pure/sign.ML	Mon Mar 10 13:55:03 2014 +0100
    13.3 @@ -192,7 +192,7 @@
    13.4  
    13.5  fun mk_const thy (c, Ts) = Const (c, const_instance thy (c, Ts));
    13.6  
    13.7 -val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    13.8 +val declared_tyname = is_some oo (Name_Space.lookup_key o #types o Type.rep_tsig o tsig_of);
    13.9  val declared_const = can o the_const_constraint;
   13.10  
   13.11  
    14.1 --- a/src/Pure/term_sharing.ML	Mon Mar 10 10:13:47 2014 +0100
    14.2 +++ b/src/Pure/term_sharing.ML	Mon Mar 10 13:55:03 2014 +0100
    14.3 @@ -19,10 +19,10 @@
    14.4  
    14.5  fun init thy =
    14.6    let
    14.7 -    val {classes = (_, algebra), types = (_, types), ...} = Type.rep_tsig (Sign.tsig_of thy);
    14.8 +    val {classes = (_, algebra), types, ...} = Type.rep_tsig (Sign.tsig_of thy);
    14.9  
   14.10      val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
   14.11 -    val tycon = perhaps (Option.map #1 o Symtab.lookup_key types);
   14.12 +    val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types);
   14.13      val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
   14.14  
   14.15      val typs = Unsynchronized.ref (Typtab.empty: unit Typtab.table);
    15.1 --- a/src/Pure/theory.ML	Mon Mar 10 10:13:47 2014 +0100
    15.2 +++ b/src/Pure/theory.ML	Mon Mar 10 13:55:03 2014 +0100
    15.3 @@ -17,8 +17,8 @@
    15.4    val requires: theory -> string -> string -> unit
    15.5    val setup: (theory -> theory) -> unit
    15.6    val get_markup: theory -> Markup.T
    15.7 +  val axiom_table: theory -> term Name_Space.table
    15.8    val axiom_space: theory -> Name_Space.T
    15.9 -  val axiom_table: theory -> term Symtab.table
   15.10    val axioms_of: theory -> (string * term) list
   15.11    val all_axioms_of: theory -> (string * term) list
   15.12    val defs_of: theory -> Defs.T
   15.13 @@ -139,10 +139,10 @@
   15.14  
   15.15  (* basic operations *)
   15.16  
   15.17 -val axiom_space = #1 o #axioms o rep_theory;
   15.18 -val axiom_table = #2 o #axioms o rep_theory;
   15.19 +val axiom_table = #axioms o rep_theory;
   15.20 +val axiom_space = Name_Space.space_of_table o axiom_table;
   15.21  
   15.22 -val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   15.23 +fun axioms_of thy = rev (Name_Space.fold_table cons (axiom_table thy) []);
   15.24  fun all_axioms_of thy = maps axioms_of (nodes_of thy);
   15.25  
   15.26  val defs_of = #defs o rep_theory;
    16.1 --- a/src/Pure/thm.ML	Mon Mar 10 10:13:47 2014 +0100
    16.2 +++ b/src/Pure/thm.ML	Mon Mar 10 13:55:03 2014 +0100
    16.3 @@ -584,8 +584,8 @@
    16.4  fun axiom theory name =
    16.5    let
    16.6      fun get_ax thy =
    16.7 -      Symtab.lookup (Theory.axiom_table thy) name
    16.8 -      |> Option.map (fn prop =>
    16.9 +      Name_Space.lookup_key (Theory.axiom_table thy) name
   16.10 +      |> Option.map (fn (_, prop) =>
   16.11             let
   16.12               val der = deriv_rule0 (Proofterm.axm_proof name prop);
   16.13               val maxidx = maxidx_of_term prop;
   16.14 @@ -602,7 +602,7 @@
   16.15  
   16.16  (*return additional axioms of this theory node*)
   16.17  fun axioms_of thy =
   16.18 -  map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy));
   16.19 +  map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy);
   16.20  
   16.21  
   16.22  (* tags *)
    17.1 --- a/src/Pure/type.ML	Mon Mar 10 10:13:47 2014 +0100
    17.2 +++ b/src/Pure/type.ML	Mon Mar 10 13:55:03 2014 +0100
    17.3 @@ -177,7 +177,7 @@
    17.4  fun build_tsig (classes, default, types) =
    17.5    let
    17.6      val log_types =
    17.7 -      Symtab.fold (fn (c, LogicalType n) => cons (c, n) | _ => I) (snd types) []
    17.8 +      Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types []
    17.9        |> Library.sort (int_ord o pairself snd) |> map fst;
   17.10    in make_tsig (classes, default, types, log_types) end;
   17.11  
   17.12 @@ -237,17 +237,17 @@
   17.13  
   17.14  (* types *)
   17.15  
   17.16 -val type_space = #1 o #types o rep_tsig;
   17.17 +val type_space = Name_Space.space_of_table o #types o rep_tsig;
   17.18  
   17.19 -fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
   17.20 -  (classes, default, (Name_Space.alias naming binding name space, types)));
   17.21 +fun type_alias naming binding name = map_tsig (fn (classes, default, types) =>
   17.22 +  (classes, default, (Name_Space.alias_table naming binding name types)));
   17.23  
   17.24  val is_logtype = member (op =) o logical_types;
   17.25  
   17.26  
   17.27  fun undecl_type c = "Undeclared type constructor: " ^ quote c;
   17.28  
   17.29 -fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
   17.30 +fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
   17.31  
   17.32  fun check_decl context (TSig {types, ...}) (c, pos) =
   17.33    Name_Space.check_reports context types (c, [pos]);
   17.34 @@ -639,14 +639,15 @@
   17.35  
   17.36  fun map_types f = map_tsig (fn (classes, default, types) =>
   17.37    let
   17.38 -    val (space', tab') = f types;
   17.39 -    val _ = Name_Space.intern space' "dummy" = "dummy" orelse
   17.40 -      error "Illegal declaration of dummy type";
   17.41 -  in (classes, default, (space', tab')) end);
   17.42 +    val types' = f types;
   17.43 +    val _ =
   17.44 +      Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
   17.45 +        error "Illegal declaration of dummy type";
   17.46 +  in (classes, default, types') end);
   17.47  
   17.48 -fun syntactic types (Type (c, Ts)) =
   17.49 -      (case Symtab.lookup types c of SOME Nonterminal => true | _ => false)
   17.50 -        orelse exists (syntactic types) Ts
   17.51 +fun syntactic tsig (Type (c, Ts)) =
   17.52 +      (case lookup_type tsig c of SOME Nonterminal => true | _ => false)
   17.53 +        orelse exists (syntactic tsig) Ts
   17.54    | syntactic _ _ = false;
   17.55  
   17.56  in
   17.57 @@ -669,14 +670,14 @@
   17.58        (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
   17.59          [] => []
   17.60        | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   17.61 -  in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
   17.62 +  in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic tsig rhs')) end);
   17.63  
   17.64  fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal;
   17.65  
   17.66  end;
   17.67  
   17.68 -fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
   17.69 -  (classes, default, (Name_Space.hide fully c space, types)));
   17.70 +fun hide_type fully c = map_tsig (fn (classes, default, types) =>
   17.71 +  (classes, default, Name_Space.hide_table fully c types));
   17.72  
   17.73  
   17.74  (* merge type signatures *)
    18.1 --- a/src/Pure/variable.ML	Mon Mar 10 10:13:47 2014 +0100
    18.2 +++ b/src/Pure/variable.ML	Mon Mar 10 13:55:03 2014 +0100
    18.3 @@ -175,7 +175,7 @@
    18.4  
    18.5  val names_of = #names o rep_data;
    18.6  val fixes_of = #fixes o rep_data;
    18.7 -val fixes_space = #1 o fixes_of;
    18.8 +val fixes_space = Name_Space.space_of_table o fixes_of;
    18.9  val binds_of = #binds o rep_data;
   18.10  val type_occs_of = #type_occs o rep_data;
   18.11  val maxidx_of = #maxidx o rep_data;
   18.12 @@ -342,8 +342,8 @@
   18.13    in if is_fixed ctxt x' then SOME x' else NONE end;
   18.14  
   18.15  fun revert_fixed ctxt x =
   18.16 -  (case Symtab.lookup (#2 (fixes_of ctxt)) x of
   18.17 -    SOME x' => if intern_fixed ctxt x' = x then x' else x
   18.18 +  (case Name_Space.lookup_key (fixes_of ctxt) x of
   18.19 +    SOME (_, x') => if intern_fixed ctxt x' = x then x' else x
   18.20    | NONE => x);
   18.21  
   18.22  fun markup_fixed ctxt x =
   18.23 @@ -351,8 +351,8 @@
   18.24    |> Markup.name (revert_fixed ctxt x);
   18.25  
   18.26  fun dest_fixes ctxt =
   18.27 -  let val (space, tab) = fixes_of ctxt
   18.28 -  in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
   18.29 +  Name_Space.fold_table (fn (x, y) => cons (y, x)) (fixes_of ctxt) []
   18.30 +  |> sort (Name_Space.entry_ord (fixes_space ctxt) o pairself #2);
   18.31  
   18.32  
   18.33  (* collect variables *)
   18.34 @@ -383,8 +383,8 @@
   18.35      let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
   18.36        ctxt
   18.37        |> map_fixes
   18.38 -        (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>>
   18.39 -          Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
   18.40 +        (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>
   18.41 +          Name_Space.alias_table Name_Space.default_naming (Binding.make (x, pos)) x')
   18.42        |> declare_fixed x
   18.43        |> declare_constraints (Syntax.free x')
   18.44    end;
   18.45 @@ -450,8 +450,8 @@
   18.46      val still_fixed = not o newly_fixed inner outer;
   18.47  
   18.48      val gen_fixes =
   18.49 -      Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
   18.50 -        (#2 (fixes_of inner)) [];
   18.51 +      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)
   18.52 +        (fixes_of inner) [];
   18.53  
   18.54      val type_occs_inner = type_occs_of inner;
   18.55      fun gen_fixesT ts =
    19.1 --- a/src/Tools/Code/code_thingol.ML	Mon Mar 10 10:13:47 2014 +0100
    19.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Mar 10 13:55:03 2014 +0100
    19.3 @@ -877,7 +877,7 @@
    19.4    let
    19.5      val thy = Proof_Context.theory_of ctxt;
    19.6      fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
    19.7 -      ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
    19.8 +      (#constants (Consts.dest (Sign.consts_of thy'))) [];
    19.9      fun belongs_here thy' c = forall
   19.10        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
   19.11      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');