xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
authorwenzelm
Fri May 21 21:22:42 2004 +0200 (2004-05-21 ago)
changeset 14784e65d77313a94
parent 14783 e7f7ed4c06f2
child 14785 d88f4c8f0591
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri May 21 21:22:10 2004 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri May 21 21:22:42 2004 +0200
     1.3 @@ -23,15 +23,15 @@
     1.4    type data
     1.5    val rep_sg: sg ->
     1.6     {self: sg_ref,
     1.7 -    tsig: Type.type_sig,
     1.8 -    const_tab: typ Symtab.table,
     1.9 +    tsig: Type.tsig,
    1.10 +    consts: (typ * stamp) Symtab.table,
    1.11      path: string list option,
    1.12      spaces: (string * NameSpace.T) list,
    1.13      data: data}
    1.14    val name_of: sg -> string
    1.15    val stamp_names_of: sg -> string list
    1.16    val exists_stamp: string -> sg -> bool
    1.17 -  val tsig_of: sg -> Type.type_sig
    1.18 +  val tsig_of: sg -> Type.tsig
    1.19    val deref: sg_ref -> sg
    1.20    val self_ref: sg -> sg_ref
    1.21    val subsig: sg * sg -> bool
    1.22 @@ -46,10 +46,9 @@
    1.23    val defaultS: sg -> sort
    1.24    val subsort: sg -> sort * sort -> bool
    1.25    val nodup_vars: term -> term
    1.26 -  val norm_sort: sg -> sort -> sort
    1.27    val of_sort: sg -> typ * sort -> bool
    1.28    val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
    1.29 -  val univ_witness: sg -> (typ * sort) option
    1.30 +  val universal_witness: sg -> (typ * sort) option
    1.31    val typ_instance: sg -> typ * typ -> bool
    1.32    val classK: string
    1.33    val typeK: string
    1.34 @@ -92,9 +91,7 @@
    1.35    val certify_class: sg -> class -> class
    1.36    val certify_sort: sg -> sort -> sort
    1.37    val certify_typ: sg -> typ -> typ
    1.38 -  val certify_typ_no_norm: sg -> typ -> typ
    1.39 -  val certify_tycon: sg -> string -> string
    1.40 -  val certify_tyabbr: sg -> string -> string
    1.41 +  val certify_typ_raw: sg -> typ -> typ
    1.42    val certify_tyname: sg -> string -> string
    1.43    val certify_const: sg -> string -> string
    1.44    val certify_term: sg -> term -> term * typ * int
    1.45 @@ -102,7 +99,7 @@
    1.46    val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
    1.47    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.48    val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    1.49 -  val read_typ_no_norm': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    1.50 +  val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    1.51    val infer_types: sg -> (indexname -> typ option) ->
    1.52      (indexname -> sort option) -> string list -> bool
    1.53      -> xterm list * typ -> term * (indexname * typ) list
    1.54 @@ -190,8 +187,8 @@
    1.55      stamps: string ref list,                    (*unique theory indentifier*)
    1.56      syn: syn} *                                 (*syntax for parsing and printing*)
    1.57     {self: sg_ref,                               (*mutable self reference*)
    1.58 -    tsig: Type.type_sig,                        (*order-sorted signature of types*)
    1.59 -    const_tab: typ Symtab.table,                (*type schemes of constants*)
    1.60 +    tsig: Type.tsig,                            (*order-sorted signature of types*)
    1.61 +    consts: (typ * stamp) Symtab.table,         (*type schemes of constants*)
    1.62      path: string list option,                   (*current name space entry prefix*)
    1.63      spaces: (string * NameSpace.T) list,        (*name spaces for consts, types etc.*)
    1.64      data: data}                                 (*anytype data*)
    1.65 @@ -215,9 +212,9 @@
    1.66    SgRef of sg ref option;
    1.67  
    1.68  (*make signature*)
    1.69 -fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    1.70 +fun make_sign (id, self, tsig, consts, syn, path, spaces, data, stamps) =
    1.71    Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
    1.72 -    const_tab = const_tab, path = path, spaces = spaces, data = data});
    1.73 +    consts = consts, path = path, spaces = spaces, data = data});
    1.74  
    1.75  
    1.76  (* basic operations *)
    1.77 @@ -231,7 +228,7 @@
    1.78  val pprint_sg = Pretty.pprint o pretty_sg;
    1.79  
    1.80  val tsig_of = #tsig o rep_sg;
    1.81 -fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
    1.82 +fun const_type (Sg (_, {consts, ...})) c = apsome #1 (Symtab.lookup (consts, c));
    1.83  
    1.84  
    1.85  (* id and self *)
    1.86 @@ -334,11 +331,10 @@
    1.87  val classes = Type.classes o tsig_of;
    1.88  val defaultS = Type.defaultS o tsig_of;
    1.89  val subsort = Type.subsort o tsig_of;
    1.90 -val norm_sort = Type.norm_sort o tsig_of;
    1.91  val of_sort = Type.of_sort o tsig_of;
    1.92  val witness_sorts = Type.witness_sorts o tsig_of;
    1.93 -val univ_witness = Type.univ_witness o tsig_of;
    1.94 -fun typ_instance sg (T, U) = Type.typ_instance (tsig_of sg, T, U);
    1.95 +val universal_witness = Type.universal_witness o tsig_of;
    1.96 +val typ_instance = Type.typ_instance o tsig_of;
    1.97  
    1.98  
    1.99  (** signature data **)
   1.100 @@ -357,8 +353,7 @@
   1.101    error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   1.102  
   1.103  fun err_uninit sg kind =
   1.104 -  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^
   1.105 -         of_theory sg);
   1.106 +  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   1.107  
   1.108  (*Trying to access theory data using get / put operations from a different
   1.109    instance of the TheoryDataFun result.  Typical cure: re-load all files*)
   1.110 @@ -454,7 +449,7 @@
   1.111    end;
   1.112  
   1.113  fun extend_sign keep extfun name decls
   1.114 -    (sg as Sg ({id = _, stamps, syn}, {self, tsig, const_tab, path, spaces, data})) =
   1.115 +    (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, path, spaces, data})) =
   1.116    let
   1.117      val _ = check_stale sg;
   1.118      val (self', data') =
   1.119 @@ -462,7 +457,7 @@
   1.120        else (SgRef (Some (ref sg)), prep_ext_data data);
   1.121    in
   1.122      create_sign self' stamps name
   1.123 -      (extfun sg (syn, tsig, const_tab, (path, spaces), data') decls)
   1.124 +      (extfun sg (syn, tsig, consts, (path, spaces), data') decls)
   1.125    end;
   1.126  
   1.127  
   1.128 @@ -494,14 +489,15 @@
   1.129  
   1.130  (*make full names*)
   1.131  fun full _ "" = error "Attempt to declare empty name \"\""
   1.132 -  | full None name = name
   1.133 -  | full (Some path) name =
   1.134 -      if NameSpace.is_qualified name then
   1.135 -        error ("Attempt to declare qualified name " ^ quote name)
   1.136 +  | full None bname = bname
   1.137 +  | full (Some path) bname =
   1.138 +      if NameSpace.is_qualified bname then
   1.139 +        error ("Attempt to declare qualified name " ^ quote bname)
   1.140        else
   1.141 -       (if not (Syntax.is_identifier name)
   1.142 -        then warning ("Declared non-identifier name " ^ quote name) else ();
   1.143 -        NameSpace.pack (path @ [name]));
   1.144 +        let val name = NameSpace.pack (path @ [bname]) in
   1.145 +          if Syntax.is_identifier bname then ()
   1.146 +          else warning ("Declared non-identifier " ^ quote name); name
   1.147 +        end;
   1.148  
   1.149  (*base name*)
   1.150  val base_name = NameSpace.base;
   1.151 @@ -579,12 +575,12 @@
   1.152  val pure_syn =
   1.153    Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   1.154  
   1.155 -val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
   1.156 +val dummy_sg = make_sign (ref "", SgRef None, Type.empty_tsig,
   1.157    Symtab.empty, pure_syn, Some [], [], empty_data, []);
   1.158  
   1.159  val pre_pure =
   1.160    create_sign (SgRef (Some (ref dummy_sg))) [] "#"
   1.161 -    (pure_syn, Type.tsig0, Symtab.empty, (Some [], []), empty_data);
   1.162 +    (pure_syn, Type.empty_tsig, Symtab.empty, (Some [], []), empty_data);
   1.163  
   1.164  val PureN = "Pure";
   1.165  val CPureN = "CPure";
   1.166 @@ -658,8 +654,8 @@
   1.167    error ("The error(s) above occurred in type " ^ quote s);
   1.168  
   1.169  fun rd_raw_typ syn tsig spaces def_sort str =
   1.170 -  intrn_tycons spaces
   1.171 -    (Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str
   1.172 +  intrn_tycons spaces (Syntax.read_typ syn
   1.173 +    (TypeInfer.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str
   1.174        handle ERROR => err_in_type str);
   1.175  
   1.176  fun read_raw_typ' syn (sg as Sg (_, {tsig, spaces, ...}), def_sort) str =
   1.177 @@ -673,10 +669,10 @@
   1.178      (cert (tsig_of sg) (rd (sg, def_sort) str)
   1.179        handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
   1.180  in
   1.181 -  val read_typ              = read_typ_aux read_raw_typ Type.cert_typ;
   1.182 -  val read_typ_no_norm      = read_typ_aux read_raw_typ Type.cert_typ_no_norm;
   1.183 -  fun read_typ' syn         = read_typ_aux (read_raw_typ' syn) Type.cert_typ;
   1.184 -  fun read_typ_no_norm' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_no_norm;
   1.185 +  val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
   1.186 +  val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
   1.187 +  fun read_typ' syn     = read_typ_aux (read_raw_typ' syn) Type.cert_typ;
   1.188 +  fun read_typ_raw' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_raw;
   1.189  end;
   1.190  
   1.191  
   1.192 @@ -686,22 +682,15 @@
   1.193  val certify_class = Type.cert_class o tsig_of;
   1.194  val certify_sort = Type.cert_sort o tsig_of;
   1.195  val certify_typ = Type.cert_typ o tsig_of;
   1.196 -val certify_typ_no_norm = Type.cert_typ_no_norm o tsig_of;
   1.197 -
   1.198 -fun certify_tycon sg c =
   1.199 -  if is_some (Symtab.lookup (#tycons (Type.rep_tsig (tsig_of sg)), c)) then c
   1.200 -  else raise TYPE ("Undeclared type constructor " ^ quote c, [], []);
   1.201 -
   1.202 -fun certify_tyabbr sg c =
   1.203 -  if is_some (Symtab.lookup (#abbrs (Type.rep_tsig (tsig_of sg)), c)) then c
   1.204 -  else raise TYPE ("Unknown type abbreviation " ^ quote c, [], []);
   1.205 +val certify_typ_raw = Type.cert_typ_raw o tsig_of;
   1.206  
   1.207  fun certify_tyname sg c =
   1.208 -  certify_tycon sg c handle TYPE _ => certify_tyabbr sg c handle TYPE _ =>
   1.209 -    raise TYPE ("Unknown type name " ^ quote c, [], []);
   1.210 +  if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
   1.211 +  else raise TYPE ("Undeclared type constructor: " ^ quote c, [], []);
   1.212  
   1.213  fun certify_const sg c =
   1.214 -  if is_some (const_type sg c) then c else raise TYPE ("Undeclared constant " ^ quote c, [], []);
   1.215 +  if is_some (const_type sg c) then c
   1.216 +  else raise TYPE ("Undeclared constant: " ^ quote c, [], []);
   1.217  
   1.218  
   1.219  (* certify_term *)
   1.220 @@ -781,34 +770,34 @@
   1.221  
   1.222    in typ_of ([], tm) end;
   1.223  
   1.224 -
   1.225  fun certify_term sg tm =
   1.226    let
   1.227      val _ = check_stale sg;
   1.228 -    val tsig = tsig_of sg;
   1.229 +
   1.230 +    val tm' = Term.map_term_types (Type.cert_typ (tsig_of sg)) tm;
   1.231 +    val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
   1.232 +
   1.233 +    fun err msg = raise TYPE (msg, [], [tm']);
   1.234  
   1.235      fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T);
   1.236  
   1.237 -    fun atom_err (errs, Const (a, T)) =
   1.238 -        (case const_type sg a of
   1.239 -          None => ("Undeclared constant " ^ show_const a T) :: errs
   1.240 -        | Some U =>
   1.241 -            if typ_instance sg (T, U) then errs
   1.242 -            else ("Illegal type for constant " ^ show_const a T) :: errs)
   1.243 -      | atom_err (errs, Var ((x, i), _)) =
   1.244 -          if i < 0 then ("Negative index for Var " ^ quote x) :: errs else errs
   1.245 -      | atom_err (errs, _) = errs;
   1.246 +    fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
   1.247 +      | check_atoms (Abs (_, _, t)) = check_atoms t
   1.248 +      | check_atoms (Const (a, T)) =
   1.249 +          (case const_type sg a of
   1.250 +            None => err ("Undeclared constant " ^ show_const a T)
   1.251 +          | Some U =>
   1.252 +              if typ_instance sg (T, U) then ()
   1.253 +              else err ("Illegal type for constant " ^ show_const a T))
   1.254 +      | check_atoms (Var ((x, i), _)) =
   1.255 +          if i < 0 then err ("Malformed variable: " ^ quote x) else ()
   1.256 +      | check_atoms _ = ();
   1.257 +  in
   1.258 +    check_atoms tm';
   1.259 +    nodup_vars tm';
   1.260 +    (tm', type_check sg tm', maxidx_of_term tm')
   1.261 +  end;
   1.262  
   1.263 -    val norm_tm =
   1.264 -      (case it_term_types (Type.typ_errors tsig) (tm, []) of
   1.265 -        [] => Type.norm_term tsig tm
   1.266 -      | errs => raise TYPE (cat_lines errs, [], [tm]));
   1.267 -    val _ = nodup_vars norm_tm;
   1.268 -  in
   1.269 -    (case foldl_aterms atom_err ([], norm_tm) of
   1.270 -      [] => (norm_tm, type_check sg norm_tm, maxidx_of_term norm_tm)
   1.271 -    | errs => raise TYPE (cat_lines errs, [], [norm_tm]))
   1.272 -  end;
   1.273  
   1.274  
   1.275  (** infer_types **)         (*exception ERROR*)
   1.276 @@ -834,7 +823,7 @@
   1.277        map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   1.278  
   1.279      fun infer ts = OK
   1.280 -      (Type.infer_types prt prT tsig (const_type sg) def_type def_sort
   1.281 +      (TypeInfer.infer_types prt prT tsig (const_type sg) def_type def_sort
   1.282          (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze typs ts)
   1.283        handle TYPE (msg, _, _) => Error msg;
   1.284  
   1.285 @@ -899,7 +888,7 @@
   1.286  (* add default sort *)
   1.287  
   1.288  fun ext_defS prep_sort sg (syn, tsig, ctab, (path, spaces), data) S =
   1.289 -  (syn, Type.ext_tsig_defsort tsig (prep_sort sg syn tsig spaces S),
   1.290 +  (syn, Type.set_defsort (prep_sort sg syn tsig spaces S) tsig,
   1.291      ctab, (path, spaces), data);
   1.292  
   1.293  fun ext_defsort arg = ext_defS rd_sort arg;
   1.294 @@ -911,13 +900,10 @@
   1.295  fun ext_types _ (syn, tsig, ctab, (path, spaces), data) types =
   1.296    let val decls = decls_of path Syntax.type_name types in
   1.297      (map_syntax (Syntax.extend_type_gram types) syn,
   1.298 -      Type.ext_tsig_types tsig decls, ctab,
   1.299 +      Type.add_types decls tsig, ctab,
   1.300        (path, add_names spaces typeK (map fst decls)), data)
   1.301    end;
   1.302  
   1.303 -fun ext_nonterminals sign sg nonterms =
   1.304 -  ext_types sign sg (map (fn n => (n, 0, Syntax.NoSyn)) nonterms);
   1.305 -
   1.306  
   1.307  (* add type abbreviations *)
   1.308  
   1.309 @@ -936,13 +922,23 @@
   1.310      val spaces' = add_names spaces typeK (map #1 abbrs');
   1.311      val decls = map (rd_abbr sg syn' tsig spaces') abbrs';
   1.312    in
   1.313 -    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'), data)
   1.314 +    (syn', Type.add_abbrs decls tsig, ctab, (path, spaces'), data)
   1.315    end;
   1.316  
   1.317  fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
   1.318  fun ext_tyabbrs_i abbrs = ext_abbrs no_read abbrs;
   1.319  
   1.320  
   1.321 +(* add nonterminals *)
   1.322 +
   1.323 +fun ext_nonterminals _ (syn, tsig, ctab, (path, spaces), data) bnames =
   1.324 +  let val names = map (full path) bnames in
   1.325 +    (map_syntax (Syntax.extend_consts names) syn,
   1.326 +      Type.add_nonterminals names tsig, ctab,
   1.327 +      (path, add_names spaces typeK names), data)
   1.328 +  end;
   1.329 +
   1.330 +
   1.331  (* add type arities *)
   1.332  
   1.333  fun ext_ars int prep_sort sg (syn, tsig, ctab, (path, spaces), data) arities =
   1.334 @@ -950,7 +946,7 @@
   1.335      val prepS = prep_sort sg syn tsig spaces;
   1.336      fun prep_arity (c, Ss, S) =
   1.337        (if int then intrn spaces typeK c else c, map prepS Ss, prepS S);
   1.338 -    val tsig' = Type.ext_tsig_arities tsig (map prep_arity arities);
   1.339 +    val tsig' = Type.add_arities (map prep_arity arities) tsig;
   1.340      val log_types = Type.logical_types tsig';
   1.341    in
   1.342      (map_syntax (Syntax.extend_log_types log_types) syn,
   1.343 @@ -980,10 +976,10 @@
   1.344  fun ext_cnsts rd_const syn_only prmode sg (syn, tsig, ctab, (path, spaces), data)
   1.345      raw_consts =
   1.346    let
   1.347 -    fun prep_const (c, ty, mx) =
   1.348 -      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   1.349 -        handle TYPE (msg, _, _) =>
   1.350 -          (error_msg msg; err_in_const (const_name path c mx));
   1.351 +    val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
   1.352 +      (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
   1.353 +    fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
   1.354 +      (error_msg msg; err_in_const (const_name path c mx));
   1.355  
   1.356      val consts = map (prep_const o rd_const sg syn tsig (path, spaces)) raw_consts;
   1.357      val decls =
   1.358 @@ -991,7 +987,7 @@
   1.359        else decls_of path Syntax.const_name consts;
   1.360    in
   1.361      (map_syntax (Syntax.extend_const_gram prmode consts) syn, tsig,
   1.362 -      Symtab.extend (ctab, decls)
   1.363 +      Symtab.extend (ctab, map (fn (c, T) => (c, (T, stamp ()))) decls)
   1.364          handle Symtab.DUPS cs => err_dup_consts cs,
   1.365        (path, add_names spaces constK (map fst decls)), data)
   1.366    end;
   1.367 @@ -1031,7 +1027,7 @@
   1.368    in
   1.369      ext_consts_i sg
   1.370        (map_syntax (Syntax.extend_consts names) syn,
   1.371 -        Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data)
   1.372 +        Type.add_classes classes' tsig, ctab, (path, spaces'), data)
   1.373      consts
   1.374    end;
   1.375  
   1.376 @@ -1040,7 +1036,7 @@
   1.377  
   1.378  fun ext_classrel int _ (syn, tsig, ctab, (path, spaces), data) pairs =
   1.379    let val intrn = if int then map (pairself (intrn_class spaces)) else I in
   1.380 -    (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces), data)
   1.381 +    (syn, Type.add_classrel (intrn pairs) tsig, ctab, (path, spaces), data)
   1.382    end;
   1.383  
   1.384  
   1.385 @@ -1116,13 +1112,13 @@
   1.386  fun copy_data (k, (e, mths as (cp, _, _, _))) =
   1.387    (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
   1.388  
   1.389 -fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, const_tab, path, spaces, data})) =
   1.390 +fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, path, spaces, data})) =
   1.391    let
   1.392      val _ = check_stale sg;
   1.393      val self' = SgRef (Some (ref sg));
   1.394      val Data tab = data;
   1.395      val data' = Data (Symtab.map copy_data tab);
   1.396 -  in create_sign self' stamps "#" (syn, tsig, const_tab, (path, spaces), data') end;
   1.397 +  in create_sign self' stamps "#" (syn, tsig, consts, (path, spaces), data') end;
   1.398  
   1.399  
   1.400  (* the external interfaces *)
   1.401 @@ -1204,10 +1200,10 @@
   1.402    else
   1.403      let
   1.404        val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
   1.405 -          {self = _, tsig = tsig1, const_tab = const_tab1,
   1.406 +          {self = _, tsig = tsig1, consts = consts1,
   1.407              path = _, spaces = spaces1, data = data1}) = sg1;
   1.408        val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
   1.409 -          {self = _, tsig = tsig2, const_tab = const_tab2,
   1.410 +          {self = _, tsig = tsig2, consts = consts2,
   1.411              path = _, spaces = spaces2, data = data2}) = sg2;
   1.412  
   1.413        val id = ref "";
   1.414 @@ -1218,9 +1214,8 @@
   1.415        val syntax = Syntax.merge_syntaxes syntax1 syntax2;
   1.416        val trfuns = merge_trfuns trfuns1 trfuns2;
   1.417        val tsig = Type.merge_tsigs (tsig1, tsig2);
   1.418 -      val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   1.419 -        handle Symtab.DUPS cs =>
   1.420 -          raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []);
   1.421 +      val consts = Symtab.merge eq_snd (consts1, consts2)
   1.422 +        handle Symtab.DUPS cs => err_dup_consts cs;
   1.423  
   1.424        val path = Some [];
   1.425        val kinds = distinct (map fst (spaces1 @ spaces2));
   1.426 @@ -1231,7 +1226,7 @@
   1.427  
   1.428        val data = merge_data (data1, data2);
   1.429  
   1.430 -      val sign = make_sign (id, self, tsig, const_tab, Syn (syntax, trfuns),
   1.431 +      val sign = make_sign (id, self, tsig, consts, Syn (syntax, trfuns),
   1.432          path, spaces, data, stamps);
   1.433      in self_ref := sign; syn_of sign; sign end;
   1.434