discontinued named name spaces (classK, typeK, constK);
authorwenzelm
Sat Jun 11 22:15:53 2005 +0200 (2005-06-11)
changeset 16368a06868ebeb0f
parent 16367 e11031fe4096
child 16369 96d73621fabb
discontinued named name spaces (classK, typeK, constK);
name space of classes and types maintained in tsig;
read_tyname/read_const now raise ERROR instead of TYPE;
tuned;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sat Jun 11 22:15:52 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Jun 11 22:15:53 2005 +0200
     1.3 @@ -13,9 +13,8 @@
     1.4    val rep_sg: sg ->
     1.5     {self: sg_ref,
     1.6      tsig: Type.tsig,
     1.7 -    consts: (typ * stamp) Symtab.table,
     1.8 +    consts: (typ * stamp) NameSpace.table,
     1.9      naming: NameSpace.naming,
    1.10 -    spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
    1.11      data: data}
    1.12    val stamp_names_of: sg -> string list
    1.13    val exists_stamp: string -> sg -> bool
    1.14 @@ -59,16 +58,13 @@
    1.15    val the_const_type: sg -> string -> typ
    1.16    val declared_tyname: sg -> string -> bool
    1.17    val declared_const: sg -> string -> bool
    1.18 -  val classK: string
    1.19 -  val typeK: string
    1.20 -  val constK: string
    1.21 -  val intern: sg -> string -> xstring -> string
    1.22 -  val extern: sg -> string -> string -> xstring
    1.23 -  val extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
    1.24 +  val class_space: sg -> NameSpace.T
    1.25 +  val type_space: sg -> NameSpace.T
    1.26 +  val const_space: sg -> NameSpace.T
    1.27    val intern_class: sg -> xstring -> string
    1.28    val extern_class: sg -> string -> xstring
    1.29 -  val intern_tycon: sg -> xstring -> string
    1.30 -  val extern_tycon: sg -> string -> xstring
    1.31 +  val intern_type: sg -> xstring -> string
    1.32 +  val extern_type: sg -> string -> xstring
    1.33    val intern_const: sg -> xstring -> string
    1.34    val extern_const: sg -> string -> xstring
    1.35    val intern_sort: sg -> sort -> sort
    1.36 @@ -106,8 +102,8 @@
    1.37    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.38    val read_typ_syntax: sg * (indexname -> sort option) -> string -> typ
    1.39    val read_typ_abbrev: sg * (indexname -> sort option) -> string -> typ
    1.40 -  val read_tyname: sg -> string -> typ        (*exception TYPE*)
    1.41 -  val read_const: sg -> string -> term        (*exception TYPE*)
    1.42 +  val read_tyname: sg -> string -> typ
    1.43 +  val read_const: sg -> string -> term
    1.44    val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
    1.45      (indexname -> sort option) -> string list -> bool
    1.46      -> (term list * typ) list -> term list * (indexname * typ) list
    1.47 @@ -167,8 +163,12 @@
    1.48    val custom_accesses: (string list -> string list list) -> sg -> sg
    1.49    val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
    1.50    val restore_naming: sg -> sg -> sg
    1.51 -  val hide_space: bool -> string * string list -> sg -> sg
    1.52 -  val hide_space_i: bool -> string * string list -> sg -> sg
    1.53 +  val hide_classes: bool -> xstring list -> sg -> sg
    1.54 +  val hide_classes_i: bool -> string list -> sg -> sg
    1.55 +  val hide_types: bool -> xstring list -> sg -> sg
    1.56 +  val hide_types_i: bool -> string list -> sg -> sg
    1.57 +  val hide_consts: bool -> xstring list -> sg -> sg
    1.58 +  val hide_consts_i: bool -> string list -> sg -> sg
    1.59    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.60    val merge: sg * sg -> sg
    1.61    val prep_ext_merge: sg list -> sg
    1.62 @@ -194,13 +194,12 @@
    1.63  datatype sg =
    1.64    Sg of
    1.65     {id: string ref,
    1.66 -    stamps: string ref list,                      (*unique theory indentifier*)
    1.67 -    syn: syn} *                                   (*syntax for parsing and printing*)
    1.68 -   {self: sg_ref,                                 (*mutable self reference*)
    1.69 -    tsig: Type.tsig,                              (*order-sorted signature of types*)
    1.70 -    consts: (typ * stamp) Symtab.table,           (*type schemes of constants*)
    1.71 +    stamps: string ref list,                  (*unique theory indentifier*)
    1.72 +    syn: syn} *                               (*syntax for parsing and printing*)
    1.73 +   {self: sg_ref,                             (*mutable self reference*)
    1.74 +    tsig: Type.tsig,                          (*order-sorted signature of types*)
    1.75 +    consts: (typ * stamp) NameSpace.table,    (*type schemes of constants*)
    1.76      naming: NameSpace.naming,
    1.77 -    spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
    1.78      data: data}
    1.79  and data =
    1.80    Data of
    1.81 @@ -222,9 +221,9 @@
    1.82    SgRef of sg ref option;
    1.83  
    1.84  (* FIXME assign!??? *)
    1.85 -fun make_sg (id, self, stamps) naming data (syn, tsig, consts, spaces) =
    1.86 +fun make_sg (id, self, stamps) naming data (syn, tsig, consts) =
    1.87    Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
    1.88 -    consts = consts, naming = naming, spaces = spaces, data = data});
    1.89 +    consts = consts, naming = naming, data = data});
    1.90  
    1.91  fun rep_sg (Sg (_, args)) = args;
    1.92  
    1.93 @@ -365,37 +364,39 @@
    1.94      val sg = make_sg (id, self, id :: stamps') naming data sign;
    1.95    in assign self sg; sg end;
    1.96  
    1.97 -fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, spaces, data})) =
    1.98 +fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, data})) =
    1.99    let
   1.100      val _ = check_stale "Sign.new_sg" sg;
   1.101      val self' = SgRef (SOME (ref sg));
   1.102      val data' = f data;
   1.103 -  in create_sg "#" self' stamps naming data' (syn, tsig, consts, spaces) end;
   1.104 +  in create_sg "#" self' stamps naming data' (syn, tsig, consts) end;
   1.105  
   1.106  val prep_ext = new_sg prep_ext_data;
   1.107  val copy = new_sg copy_data;
   1.108  
   1.109 -fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   1.110 +fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
   1.111    let
   1.112      val _ = check_stale "Sign.add_name" sg;
   1.113      val (self', data') =
   1.114        if is_draft sg then (self, data)
   1.115        else (SgRef (SOME (ref sg)), prep_ext_data data);
   1.116 -  in create_sg name self' stamps naming data' (syn, tsig, consts, spaces) end;
   1.117 +  in create_sg name self' stamps naming data' (syn, tsig, consts) end;
   1.118  
   1.119 -fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   1.120 +fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, data})) =
   1.121    let
   1.122      val _ = check_stale "Sign.map_sg" sg;
   1.123      val (self', data') =
   1.124        if is_draft sg andalso keep then (self, data)
   1.125        else (SgRef (SOME (ref sg)), prep_ext_data data);
   1.126 -    val (naming', data', sign') = f (naming, data', (syn, tsig, consts, spaces));
   1.127 +    val (naming', data', sign') = f (naming, data', (syn, tsig, consts));
   1.128    in create_sg "#" self' stamps naming' data' sign' end;
   1.129  
   1.130  fun map_naming f = map_sg true (fn (naming, data, sign) => (f naming, data, sign));
   1.131  fun map_data f = map_sg true (fn (naming, data, sign) => (naming, f data, sign));
   1.132  fun map_sign f = map_sg true (fn (naming, data, sign) => (naming, data, f sign));
   1.133 -fun map_syn f = map_sign (fn (syn, tsig, consts, spaces) => (f syn, tsig, consts, spaces));
   1.134 +fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
   1.135 +fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
   1.136 +fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
   1.137  
   1.138  
   1.139  
   1.140 @@ -453,25 +454,15 @@
   1.141  
   1.142  (** primitive signatures **)
   1.143  
   1.144 -val empty_spaces =
   1.145 -  {class = NameSpace.empty, tycon = NameSpace.empty, const = NameSpace.empty};
   1.146 -
   1.147 -fun merge_spaces
   1.148 -  ({class = class1, tycon = tycon1, const = const1},
   1.149 -    {class = class2, tycon = tycon2, const = const2}) =
   1.150 -  {class = NameSpace.merge (class1, class2),
   1.151 -   tycon = NameSpace.merge (tycon1, tycon2),
   1.152 -   const = NameSpace.merge (const1, const2)};
   1.153 -
   1.154  val pure_syn =
   1.155    Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   1.156  
   1.157  val dummy_sg = make_sg (ref "", SgRef NONE, []) NameSpace.default_naming empty_data
   1.158 -  (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
   1.159 +  (pure_syn, Type.empty_tsig, NameSpace.empty_table);
   1.160  
   1.161  val pre_pure =
   1.162    create_sg "#" (SgRef (SOME (ref dummy_sg))) [] NameSpace.default_naming empty_data
   1.163 -    (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
   1.164 +    (pure_syn, Type.empty_tsig, NameSpace.empty_table);
   1.165  
   1.166  val PureN = "Pure";
   1.167  val CPureN = "CPure";
   1.168 @@ -538,56 +529,31 @@
   1.169  
   1.170  (* consts signature *)
   1.171  
   1.172 -fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
   1.173 +fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (#2 consts, c));
   1.174  
   1.175  fun the_const_type sg c =
   1.176    (case const_type sg c of SOME T => T
   1.177    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   1.178  
   1.179 -fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
   1.180 -fun declared_const sg c = is_some (const_type sg c);
   1.181 -
   1.182 -
   1.183 -(* name spaces *)
   1.184 -
   1.185 -val classK = "class";
   1.186 -val typeK = "type";
   1.187 -val constK = "const";
   1.188 -
   1.189 -fun illegal_space kind = "Illegal signature name space: " ^ quote kind;
   1.190 +fun declared_tyname sg c =
   1.191 +  is_some (Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c));
   1.192  
   1.193 -fun space_of sg kind = #spaces (rep_sg sg) |>
   1.194 - (if kind = classK then #class
   1.195 -  else if kind = typeK then #tycon
   1.196 -  else if kind = constK then #const
   1.197 -  else raise TERM (illegal_space kind, []));
   1.198 -
   1.199 -fun map_space kind f {class, tycon, const} =
   1.200 -  let
   1.201 -    val (class', tycon', const') =
   1.202 -      if kind = classK then (f class, tycon, const)
   1.203 -      else if kind = typeK then (class, f tycon, const)
   1.204 -      else if kind = constK then (class, tycon, f const)
   1.205 -      else raise TERM (illegal_space kind, []);
   1.206 -  in {class = class', tycon = tycon', const = const'} end;
   1.207 -
   1.208 -fun declare_names sg kind = map_space kind o fold (declare_name sg);
   1.209 -fun hide_names kind = map_space kind oo (fold o NameSpace.hide);
   1.210 +fun declared_const sg c = is_some (const_type sg c);
   1.211  
   1.212  
   1.213  
   1.214  (** intern / extern names **)
   1.215  
   1.216 -val intern = NameSpace.intern oo space_of;
   1.217 -val extern = NameSpace.extern oo space_of;
   1.218 -fun extern_table sg = curry NameSpace.extern_table o space_of sg;
   1.219 +val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
   1.220 +val type_space = #1 o #types o Type.rep_tsig o tsig_of;
   1.221 +val const_space = #1 o #consts o rep_sg
   1.222  
   1.223 -fun intern_class sg = intern sg classK;
   1.224 -fun extern_class sg = extern sg classK;
   1.225 -fun intern_tycon sg = intern sg typeK;
   1.226 -fun extern_tycon sg = extern sg typeK;
   1.227 -fun intern_const sg = intern sg constK;
   1.228 -fun extern_const sg = extern sg constK;
   1.229 +val intern_class = NameSpace.intern o class_space;
   1.230 +val extern_class = NameSpace.extern o class_space;
   1.231 +val intern_type = NameSpace.intern o type_space;
   1.232 +val extern_type = NameSpace.extern o type_space;
   1.233 +val intern_const = NameSpace.intern o const_space;
   1.234 +val extern_const = NameSpace.extern o const_space;
   1.235  
   1.236  val intern_sort = map o intern_class;
   1.237  val extern_sort = map o extern_class;
   1.238 @@ -614,11 +580,11 @@
   1.239  
   1.240  in
   1.241  
   1.242 -val intern_typ = typ_mapping intern_class intern_tycon;
   1.243 -val extern_typ = typ_mapping extern_class extern_tycon;
   1.244 -val intern_term = term_mapping intern_class intern_tycon intern_const;
   1.245 -val extern_term = term_mapping extern_class extern_tycon extern_const;
   1.246 -val intern_tycons = typ_mapping (K I) intern_tycon;
   1.247 +val intern_typ = typ_mapping intern_class intern_type;
   1.248 +val extern_typ = typ_mapping extern_class extern_type;
   1.249 +val intern_term = term_mapping intern_class intern_type intern_const;
   1.250 +val extern_term = term_mapping extern_class extern_type extern_const;
   1.251 +val intern_tycons = typ_mapping (K I) intern_type;
   1.252  
   1.253  end;
   1.254  
   1.255 @@ -636,7 +602,7 @@
   1.256  
   1.257  fun pretty_arity sg (a, Ss, S) =
   1.258    let
   1.259 -    val a' = extern_tycon sg a;
   1.260 +    val a' = extern_type sg a;
   1.261      val dom =
   1.262        if null Ss then []
   1.263        else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
   1.264 @@ -734,7 +700,7 @@
   1.265  
   1.266  
   1.267  
   1.268 -(** read and certify entities **)    (*exception ERROR*)
   1.269 +(** read and certify entities **)    (*exception ERROR/TYPE*)
   1.270  
   1.271  (* sorts *)
   1.272  
   1.273 @@ -775,18 +741,20 @@
   1.274  end;
   1.275  
   1.276  
   1.277 -(* type and constant names *)    (*exception TYPE*)   (* FIXME really!? *)
   1.278 +(* type and constant names *)
   1.279  
   1.280  fun read_tyname sg raw_c =
   1.281 -  let val c = intern_tycon sg raw_c in
   1.282 -    (case Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c) of
   1.283 +  let val c = intern_type sg raw_c in
   1.284 +    (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of sg))), c) of
   1.285        SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
   1.286 -    | _ => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
   1.287 +    | _ => error ("Undeclared type constructor: " ^ quote c))
   1.288    end;
   1.289  
   1.290  fun read_const sg raw_c =
   1.291 -  let val c = intern_const sg raw_c
   1.292 -  in the_const_type sg c; Const (c, dummyT) end;
   1.293 +  let
   1.294 +    val c = intern_const sg raw_c;
   1.295 +    val _ = the_const_type sg c handle TYPE (msg, _, _) => error msg;
   1.296 +  in Const (c, dummyT) end;
   1.297  
   1.298  
   1.299  
   1.300 @@ -867,8 +835,8 @@
   1.301  
   1.302  (* add default sort *)
   1.303  
   1.304 -fun gen_add_defsort prep_sort s sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.305 -  (syn, Type.set_defsort (prep_sort sg s) tsig, consts, spaces));
   1.306 +fun gen_add_defsort prep_sort s sg =
   1.307 +  sg |> map_tsig (Type.set_defsort (prep_sort sg s));
   1.308  
   1.309  val add_defsort = gen_add_defsort read_sort;
   1.310  val add_defsort_i = gen_add_defsort certify_sort;
   1.311 @@ -876,38 +844,34 @@
   1.312  
   1.313  (* add type constructors *)
   1.314  
   1.315 -fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.316 +fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts) =>
   1.317    let
   1.318      val syn' = map_syntax (Syntax.extend_type_gram types) syn;
   1.319 -    val decls = map (fn (a, n, mx) => (full_name sg (Syntax.type_name a mx), n)) types;
   1.320 -    val tsig' = Type.add_types decls tsig;
   1.321 -    val spaces' = declare_names sg typeK (map #1 decls) spaces;
   1.322 -  in (syn', tsig', consts, spaces') end);
   1.323 +    val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
   1.324 +    val tsig' = Type.add_types (naming_of sg) decls tsig;
   1.325 +  in (syn', tsig', consts) end);
   1.326  
   1.327  
   1.328  (* add nonterminals *)
   1.329  
   1.330 -fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.331 +fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts) =>
   1.332    let
   1.333      val syn' = map_syntax (Syntax.extend_consts bnames) syn;
   1.334 -    val names = map (full_name sg) bnames;
   1.335 -    val tsig' = Type.add_nonterminals names tsig;
   1.336 -    val spaces' = declare_names sg typeK names spaces;
   1.337 -  in (syn', tsig', consts, spaces') end);
   1.338 +    val tsig' = Type.add_nonterminals (naming_of sg) bnames tsig;
   1.339 +  in (syn', tsig', consts) end);
   1.340  
   1.341  
   1.342  (* add type abbreviations *)
   1.343  
   1.344  fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) sg =
   1.345 -  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.346 +  sg |> map_sign (fn (syn, tsig, consts) =>
   1.347      let
   1.348        val syn' = map_syntax (Syntax.extend_type_gram [(a, length vs, mx)]) syn;
   1.349 -      val a' = full_name sg (Syntax.type_name a mx);
   1.350 +      val a' = Syntax.type_name a mx;
   1.351        val abbr = (a', vs, prep_typ sg rhs) handle ERROR =>
   1.352 -        error ("in type abbreviation " ^ quote (Syntax.type_name a' mx));
   1.353 -      val tsig' = Type.add_abbrevs [abbr] tsig;
   1.354 -      val spaces' = declare_names sg typeK [a'] spaces;
   1.355 -    in (syn', tsig', consts, spaces') end);
   1.356 +        error ("in type abbreviation " ^ quote a');
   1.357 +      val tsig' = Type.add_abbrevs (naming_of sg) [abbr] tsig;
   1.358 +    in (syn', tsig', consts) end);
   1.359  
   1.360  val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
   1.361  val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
   1.362 @@ -915,15 +879,14 @@
   1.363  
   1.364  (* add type arities *)
   1.365  
   1.366 -fun gen_add_arities int_tycon prep_sort arities sg =
   1.367 -  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.368 -    let
   1.369 -      fun prep_arity (a, Ss, S) = (int_tycon sg a, map (prep_sort sg) Ss, prep_sort sg S)
   1.370 -        handle ERROR => error ("in arity for type " ^ quote a);
   1.371 -      val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
   1.372 -    in (syn, tsig', consts, spaces) end);
   1.373 +fun gen_add_arities int_type prep_sort arities sg = sg |> map_tsig (fn tsig =>
   1.374 +  let
   1.375 +    fun prep_arity (a, Ss, S) = (int_type sg a, map (prep_sort sg) Ss, prep_sort sg S)
   1.376 +      handle ERROR => error ("in arity for type " ^ quote a);
   1.377 +    val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
   1.378 +  in tsig' end);
   1.379  
   1.380 -val add_arities = gen_add_arities intern_tycon read_sort;
   1.381 +val add_arities = gen_add_arities intern_type read_sort;
   1.382  val add_arities_i = gen_add_arities (K I) certify_sort;
   1.383  
   1.384  
   1.385 @@ -956,15 +919,10 @@
   1.386      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
   1.387        handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
   1.388      val args = map prep raw_args;
   1.389 -    val decls = args |> map (fn (c, T, mx) =>
   1.390 -      (full_name sg (Syntax.const_name c mx), (T, stamp ())));
   1.391 -  in
   1.392 -    sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.393 -      (syn, tsig,
   1.394 -        Symtab.extend (consts, decls) handle Symtab.DUPS cs => err_dup_consts cs,
   1.395 -        declare_names sg constK (map #1 decls) spaces))
   1.396 -    |> add_syntax_i args
   1.397 -  end;
   1.398 +    val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, (T, stamp ())));
   1.399 +    fun extend_consts consts = NameSpace.extend_table (naming_of sg) (consts, decls)
   1.400 +      handle Symtab.DUPS cs => err_dup_consts cs;
   1.401 +  in sg |> map_consts extend_consts |> add_syntax_i args end;
   1.402  
   1.403  val add_consts = gen_add_consts (read_typ o no_def_sort);
   1.404  val add_consts_i = gen_add_consts certify_typ;
   1.405 @@ -979,14 +937,12 @@
   1.406    handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   1.407  
   1.408  fun gen_add_class int_class (bclass, raw_classes) sg =
   1.409 -  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.410 +  sg |> map_sign (fn (syn, tsig, consts) =>
   1.411      let
   1.412 -      val class = full_name sg bclass;
   1.413        val classes = map (int_class sg) raw_classes;
   1.414        val syn' = map_syntax (Syntax.extend_consts [bclass]) syn;
   1.415 -      val tsig' = Type.add_classes (pp sg) [(class, classes)] tsig;
   1.416 -      val spaces' = declare_names sg classK [class] spaces;
   1.417 -    in (syn', tsig', consts, spaces') end)
   1.418 +      val tsig' = Type.add_classes (pp sg) (naming_of sg) [(bclass, classes)] tsig;
   1.419 +    in (syn', tsig', consts) end)
   1.420    |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
   1.421  
   1.422  val add_classes = fold (gen_add_class intern_class);
   1.423 @@ -995,12 +951,11 @@
   1.424  
   1.425  (* add to classrel *)
   1.426  
   1.427 -fun gen_add_classrel int_class raw_pairs sg =
   1.428 -  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.429 -    let
   1.430 -      val pairs = map (pairself (int_class sg)) raw_pairs;
   1.431 -      val tsig' = Type.add_classrel (pp sg) pairs tsig;
   1.432 -    in (syn, tsig', consts, spaces) end);
   1.433 +fun gen_add_classrel int_class raw_pairs sg = sg |> map_tsig (fn tsig =>
   1.434 +  let
   1.435 +    val pairs = map (pairself (int_class sg)) raw_pairs;
   1.436 +    val tsig' = Type.add_classrel (pp sg) pairs tsig;
   1.437 +  in tsig' end);
   1.438  
   1.439  val add_classrel = gen_add_classrel intern_class;
   1.440  val add_classrel_i = gen_add_classrel (K I);
   1.441 @@ -1035,7 +990,7 @@
   1.442  (* add translation rules *)
   1.443  
   1.444  fun add_trrules args sg = sg |> map_syn (fn syn =>
   1.445 -  let val rules = map (Syntax.map_trrule (apfst (intern_tycon sg))) args
   1.446 +  let val rules = map (Syntax.map_trrule (apfst (intern_type sg))) args
   1.447    in map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn) rules) syn end);
   1.448  
   1.449  val add_trrules_i = map_syn o map_syntax o Syntax.extend_trrules_i;
   1.450 @@ -1053,14 +1008,13 @@
   1.451  
   1.452  (* hide names *)
   1.453  
   1.454 -fun hide_space fully (kind, xnames) sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   1.455 -  let
   1.456 -    val names = map (intern sg kind) xnames;
   1.457 -    val spaces' = hide_names kind fully names spaces;
   1.458 -  in (syn, tsig, consts, spaces') end);
   1.459 -
   1.460 -fun hide_space_i fully (kind, names) = map_sign (fn (syn, tsig, consts, spaces) =>
   1.461 -  (syn, tsig, consts, hide_names kind fully names spaces));
   1.462 +fun hide_classes b xs sg = sg |> map_tsig (Type.hide_classes b (map (intern_class sg) xs));
   1.463 +val hide_classes_i = map_tsig oo Type.hide_classes;
   1.464 +fun hide_types b xs sg = sg |> map_tsig (Type.hide_types b (map (intern_type sg) xs));
   1.465 +val hide_types_i = map_tsig oo Type.hide_types;
   1.466 +fun hide_consts b xs sg =
   1.467 +  sg |> map_consts (apfst (fold (NameSpace.hide b o intern_const sg) xs));
   1.468 +val hide_consts_i = (map_consts o apfst) oo (fold o NameSpace.hide);
   1.469  
   1.470  
   1.471  
   1.472 @@ -1101,28 +1055,25 @@
   1.473    else
   1.474      let
   1.475        val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
   1.476 -          {self = _, tsig = tsig1, consts = consts1,
   1.477 -            naming = _, spaces = spaces1, data = data1}) = sg1;
   1.478 +          {self = _, tsig = tsig1, consts = consts1, naming = _, data = data1}) = sg1;
   1.479        val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
   1.480 -          {self = _, tsig = tsig2, consts = consts2,
   1.481 -            naming = _, spaces = spaces2, data = data2}) = sg2;
   1.482 +          {self = _, tsig = tsig2, consts = consts2, naming = _, data = data2}) = sg2;
   1.483  
   1.484        val stamps = merge_stamps stamps1 stamps2;
   1.485        val syntax = Syntax.merge_syntaxes syntax1 syntax2;
   1.486        val trfuns = merge_trfuns trfuns1 trfuns2;
   1.487        val syn = Syn (syntax, trfuns);
   1.488 -      val consts = Symtab.merge eq_snd (consts1, consts2)
   1.489 +      val consts = NameSpace.merge_tables eq_snd (consts1, consts2)
   1.490          handle Symtab.DUPS cs => err_dup_consts cs;
   1.491        val naming = NameSpace.default_naming;
   1.492 -      val spaces = merge_spaces (spaces1, spaces2);
   1.493        val data = merge_data (data1, data2);
   1.494  
   1.495        val pre_sg = make_sg (ref "", SgRef (SOME (ref dummy_sg)), ref "#" :: stamps1)
   1.496 -        naming data (syn, tsig1, consts, spaces);
   1.497 +        naming data (syn, tsig1, consts);
   1.498        val tsig = Type.merge_tsigs (pp pre_sg) (tsig1, tsig2);
   1.499  
   1.500        val self = SgRef (SOME (ref dummy_sg));
   1.501 -      val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts, spaces);
   1.502 +      val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts);
   1.503      in assign self sg; syn_of sg; sg end;
   1.504  
   1.505  in