hide id, stamps;
authorwenzelm
Thu Oct 23 12:13:15 1997 +0200 (1997-10-23)
changeset 3975ddeb5a0fd08d
parent 3974 d3c2159b75fa
child 3976 1030dd79720b
hide id, stamps;
added stamp_names_of, name_of;
replaced make_draft by prep_ext;
improved print_sg;
tuned;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Oct 23 12:10:55 1997 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Oct 23 12:13:15 1997 +0200
     1.3 @@ -20,15 +20,15 @@
     1.4    type sg
     1.5    type sg_ref
     1.6    val rep_sg: sg ->
     1.7 -   {id: string ref,			(* FIXME hide!? *)
     1.8 -    self: sg_ref,
     1.9 +   {self: sg_ref,
    1.10      tsig: Type.type_sig,
    1.11      const_tab: typ Symtab.table,
    1.12      syn: Syntax.syntax,
    1.13      path: string list,
    1.14      spaces: (string * NameSpace.T) list,
    1.15 -    data: Data.T,
    1.16 -    stamps: string ref list}		(* FIXME hide!? *)
    1.17 +    data: Data.T}
    1.18 +  val name_of: sg -> string
    1.19 +  val stamp_names_of: sg -> string list
    1.20    val tsig_of: sg -> Type.type_sig
    1.21    val deref: sg_ref -> sg
    1.22    val self_ref: sg -> sg_ref
    1.23 @@ -115,7 +115,7 @@
    1.24    val put_data: string * exn -> sg -> sg
    1.25    val print_data: sg -> string -> unit
    1.26    val merge_refs: sg_ref * sg_ref -> sg_ref
    1.27 -  val make_draft: sg -> sg
    1.28 +  val prep_ext: sg -> sg
    1.29    val merge: sg * sg -> sg
    1.30    val proto_pure: sg
    1.31    val pure: sg
    1.32 @@ -131,40 +131,47 @@
    1.33  (** datatype sg **)
    1.34  
    1.35  datatype sg =
    1.36 -  Sg of {
    1.37 -    id: string ref,				(*id*)
    1.38 -    self: sg_ref,				(*mutable self reference*)
    1.39 +  Sg of
    1.40 +   {id: string ref,                             (*id*)
    1.41 +    stamps: string ref list} *                  (*unique theory indentifier*)
    1.42 +   {self: sg_ref,                               (*mutable self reference*)
    1.43      tsig: Type.type_sig,                        (*order-sorted signature of types*)
    1.44      const_tab: typ Symtab.table,                (*type schemes of constants*)
    1.45      syn: Syntax.syntax,                         (*syntax for parsing and printing*)
    1.46 -    path: string list,                     	(*current name space entry prefix*)
    1.47 -    spaces: (string * NameSpace.T) list,   	(*name spaces for consts, types etc.*)
    1.48 -    data: Data.T,				(*additional data*)
    1.49 -    stamps: string ref list}                    (*unique theory indentifier*)
    1.50 -      (*the "ref" in stamps ensures that no two signatures are identical
    1.51 -        -- it is impossible to forge a signature*)
    1.52 +    path: string list,                          (*current name space entry prefix*)
    1.53 +    spaces: (string * NameSpace.T) list,        (*name spaces for consts, types etc.*)
    1.54 +    data: Data.T}                               (*additional data*)
    1.55  and sg_ref =
    1.56    SgRef of sg ref option;
    1.57  
    1.58  (*make signature*)
    1.59  fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
    1.60 -  Sg {id = id, self = self, tsig = tsig, const_tab = const_tab, syn = syn,
    1.61 -    path = path, spaces = spaces, data = data, stamps = stamps};
    1.62 +  Sg ({id = id, stamps = stamps}, {self = self, tsig = tsig, const_tab = const_tab,
    1.63 +    syn = syn, path = path, spaces = spaces, data = data});
    1.64 +
    1.65 +
    1.66 +(* basic components *)
    1.67 +
    1.68 +fun rep_sg (Sg (_, args)) = args;
    1.69  
    1.70 -(*dest signature*)
    1.71 -fun rep_sg (Sg args) = args;
    1.72 +(*show stamps*)
    1.73 +fun stamp_names_of (Sg ({stamps, ...}, _)) = rev (map ! stamps);
    1.74 +fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
    1.75 +val str_of_sg = Pretty.str_of o pretty_sg;
    1.76 +val pprint_sg = Pretty.pprint o pretty_sg;
    1.77 +
    1.78 +
    1.79  val tsig_of = #tsig o rep_sg;
    1.80  val self_ref = #self o rep_sg;
    1.81 -
    1.82 -fun get_data (Sg {data, ...}) = Data.get data;
    1.83 -fun print_data (Sg {data, ...}) = Data.print data;
    1.84 -
    1.85 +val get_data = Data.get o #data o rep_sg;
    1.86 +val print_data = Data.print o #data o rep_sg;
    1.87  
    1.88 -(*show stamps*)
    1.89 -fun stamp_names stamps = rev (map ! stamps);
    1.90 +fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
    1.91 +val classes = #classes o Type.rep_tsig o tsig_of;
    1.92  
    1.93 -fun pretty_sg (Sg {stamps, ...}) = Pretty.str_list "{" "}" (stamp_names stamps);
    1.94 -val pprint_sg = Pretty.pprint o pretty_sg;
    1.95 +val subsort = Type.subsort o tsig_of;
    1.96 +val norm_sort = Type.norm_sort o tsig_of;
    1.97 +val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.98  
    1.99  
   1.100  (* signature id *)
   1.101 @@ -172,11 +179,17 @@
   1.102  fun deref (SgRef (Some (ref sg))) = sg
   1.103    | deref (SgRef None) = sys_error "Sign.deref";
   1.104  
   1.105 -fun check_stale (sg as Sg {id, self = SgRef (Some (ref (Sg {id = id', ...}))), ...}) =
   1.106 +fun check_stale (sg as Sg ({id, ...},
   1.107 +        {self = SgRef (Some (ref (Sg ({id = id', ...}, _)))), ...})) =
   1.108        if id = id' then sg
   1.109 -      else raise TERM ("Stale signature: " ^ Pretty.str_of (pretty_sg sg), [])
   1.110 +      else raise TERM ("Stale signature: " ^ str_of_sg sg, [])
   1.111    | check_stale _ = sys_error "Sign.check_stale";
   1.112  
   1.113 +fun name_of (sg as Sg ({id = ref name, ...}, _)) =
   1.114 +  if name = "" orelse name = "#" then
   1.115 +    raise TERM ("Nameless signature " ^ str_of_sg sg, [])
   1.116 +  else name;
   1.117 +
   1.118  
   1.119  (* inclusion and equality *)
   1.120  
   1.121 @@ -196,13 +209,13 @@
   1.122          if x = y then fast_sub (xs, ys)
   1.123          else fast_sub (x :: xs, ys);
   1.124  in
   1.125 -  fun eq_sg (sg1 as Sg {id = id1, ...}, sg2 as Sg {id = id2, ...}) =
   1.126 +  fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
   1.127      (check_stale sg1; check_stale sg2; id1 = id2);
   1.128  
   1.129 -  fun subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.130 +  fun subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   1.131      eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
   1.132  
   1.133 -  fun fast_subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.134 +  fun fast_subsig (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   1.135      eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
   1.136  end;
   1.137  
   1.138 @@ -210,11 +223,11 @@
   1.139  (*test if same theory names are contained in signatures' stamps,
   1.140    i.e. if signatures belong to same theory but not necessarily to the
   1.141    same version of it*)
   1.142 -fun same_sg (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
   1.143 +fun same_sg (sg1 as Sg ({stamps = s1, ...}, _), sg2 as Sg ({stamps = s2, ...}, _)) =
   1.144    eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
   1.145  
   1.146  (*test for drafts*)
   1.147 -fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   1.148 +fun is_draft (Sg ({stamps = ref "#" :: _, ...}, _)) = true
   1.149    | is_draft _ = false;
   1.150  
   1.151  
   1.152 @@ -239,12 +252,12 @@
   1.153      sign
   1.154    end;
   1.155  
   1.156 -fun extend_sign extfun name decls
   1.157 -    (sg as Sg {id = _, self, tsig, const_tab, syn, path, spaces, data, stamps}) =
   1.158 +fun extend_sign keep extfun name decls
   1.159 +    (sg as Sg ({id = _, stamps}, {self, tsig, const_tab, syn, path, spaces, data})) =
   1.160    let
   1.161      val _ = check_stale sg;
   1.162      val (self', data') =
   1.163 -      if is_draft sg then (self, data)
   1.164 +      if is_draft sg andalso keep then (self, data)
   1.165        else (SgRef (Some (ref sg)), Data.prep_ext data);
   1.166    in
   1.167      create_sign self' stamps name
   1.168 @@ -252,20 +265,6 @@
   1.169    end;
   1.170  
   1.171  
   1.172 -(* consts *)
   1.173 -
   1.174 -fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
   1.175 -
   1.176 -
   1.177 -(* classes and sorts *)
   1.178 -
   1.179 -val classes = #classes o Type.rep_tsig o tsig_of;
   1.180 -
   1.181 -val subsort = Type.subsort o tsig_of;
   1.182 -val norm_sort = Type.norm_sort o tsig_of;
   1.183 -val nonempty_sort = Type.nonempty_sort o tsig_of;
   1.184 -
   1.185 -
   1.186  
   1.187  (** name spaces **)
   1.188  
   1.189 @@ -360,7 +359,7 @@
   1.190        (mapping (trn constK) add_term_consts t);
   1.191  
   1.192  
   1.193 -  fun spaces_of (Sg {spaces, ...}) = spaces;
   1.194 +  val spaces_of = #spaces o rep_sg;
   1.195  
   1.196  in
   1.197  
   1.198 @@ -392,7 +391,7 @@
   1.199  
   1.200    val intern_tycons = intrn_tycons o spaces_of;
   1.201  
   1.202 -  fun full_name (Sg {path, ...}) = full path;
   1.203 +  val full_name = full o #path o rep_sg;
   1.204  
   1.205  end;
   1.206  
   1.207 @@ -400,16 +399,16 @@
   1.208  
   1.209  (** pretty printing of terms and types **)
   1.210  
   1.211 -fun pretty_term (Sg {syn, spaces, stamps, ...}) t =
   1.212 +fun pretty_term (sg as Sg (_, {syn, spaces, ...})) t =
   1.213    Syntax.pretty_term syn
   1.214 -    ("CPure" mem_string (map ! stamps))
   1.215 +    ("CPure" mem_string (stamp_names_of sg))
   1.216      (if ! long_names then t else extrn_term spaces t);
   1.217  
   1.218 -fun pretty_typ (Sg {syn, spaces, ...}) T =
   1.219 +fun pretty_typ (Sg (_, {syn, spaces, ...})) T =
   1.220    Syntax.pretty_typ syn
   1.221      (if ! long_names then T else extrn_typ spaces T);
   1.222  
   1.223 -fun pretty_sort (Sg {syn, spaces, ...}) S =
   1.224 +fun pretty_sort (Sg (_, {syn, spaces, ...})) S =
   1.225    Syntax.pretty_sort syn
   1.226      (if ! long_names then S else extrn_sort spaces S);
   1.227  
   1.228 @@ -446,10 +445,12 @@
   1.229    let
   1.230      fun prt_cls c = pretty_sort sg [c];
   1.231      fun prt_sort S = pretty_sort sg S;
   1.232 -    fun prt_tycon t = Pretty.str (cond_extern sg typeK t);
   1.233      fun prt_arity t (c, Ss) = pretty_arity sg (t, Ss, [c]);
   1.234      fun prt_typ ty = Pretty.quote (pretty_typ sg ty);
   1.235 -    fun prt_const c = Pretty.quote (Pretty.str (cond_extern sg constK c));
   1.236 +
   1.237 +    val ext_class = cond_extern sg classK;
   1.238 +    val ext_tycon = cond_extern sg typeK;
   1.239 +    val ext_const = cond_extern sg constK;
   1.240  
   1.241  
   1.242      fun pretty_space (kind, space) = Pretty.block (Pretty.breaks
   1.243 @@ -466,7 +467,7 @@
   1.244        [Pretty.str "default:", Pretty.brk 1, pretty_sort sg S];
   1.245  
   1.246      fun pretty_ty (t, n) = Pretty.block
   1.247 -      [prt_tycon t, Pretty.str (" " ^ string_of_int n)];
   1.248 +      [Pretty.str (ext_tycon t), Pretty.str (" " ^ string_of_int n)];
   1.249  
   1.250      fun pretty_abbr (t, (vs, rhs)) = Pretty.block
   1.251        [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
   1.252 @@ -475,14 +476,15 @@
   1.253      fun pretty_arities (t, ars) = map (prt_arity t) ars;
   1.254  
   1.255      fun pretty_const (c, ty) = Pretty.block
   1.256 -      [prt_const c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
   1.257 +      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
   1.258  
   1.259 -    val Sg {id = _, self = _, tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
   1.260 +    val Sg (_, {self = _, tsig, const_tab, syn = _, path, spaces, data}) = sg;
   1.261      val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
   1.262      val {classes, classrel, default, tycons, abbrs, arities} =
   1.263        Type.rep_tsig tsig;
   1.264 +    val consts = sort_wrt fst (map (apfst ext_const) (Symtab.dest const_tab));
   1.265    in
   1.266 -    Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   1.267 +    Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names_of sg));
   1.268      Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data));
   1.269      Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
   1.270      Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
   1.271 @@ -492,7 +494,7 @@
   1.272      Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
   1.273      Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs));
   1.274      Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities arities)));
   1.275 -    Pretty.writeln (Pretty.big_list "consts:" (map pretty_const (Symtab.dest const_tab)))
   1.276 +    Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
   1.277    end;
   1.278  
   1.279  
   1.280 @@ -508,7 +510,7 @@
   1.281        handle ERROR => err_in_type str);
   1.282    
   1.283  (*read and certify typ wrt a signature*)
   1.284 -fun read_typ (sg as Sg {tsig, syn, spaces, ...}, def_sort) str =
   1.285 +fun read_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str =
   1.286    (check_stale sg;
   1.287      Type.cert_typ tsig (read_raw_typ syn tsig spaces def_sort str)
   1.288        handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
   1.289 @@ -517,7 +519,7 @@
   1.290  
   1.291  (** certify types and terms **)   (*exception TYPE*)
   1.292  
   1.293 -fun certify_typ (Sg {tsig, ...}) ty = Type.cert_typ tsig ty;
   1.294 +val certify_typ = Type.cert_typ o tsig_of;
   1.295  
   1.296  (*check for duplicate TVars with distinct sorts*)
   1.297  fun nodup_TVars (tvars, T) =
   1.298 @@ -564,19 +566,19 @@
   1.299    | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
   1.300  
   1.301  
   1.302 -fun certify_term (sg as Sg {tsig, ...}) tm =
   1.303 +fun certify_term sg tm =
   1.304    let
   1.305      val _ = check_stale sg;
   1.306 +    val tsig = tsig_of sg;
   1.307  
   1.308 -    fun valid_const a T =
   1.309 -      (case const_type sg a of
   1.310 -        Some U => Type.typ_instance (tsig, T, U)
   1.311 -      | _ => false);
   1.312 +    fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T);
   1.313  
   1.314      fun atom_err (Const (a, T)) =
   1.315 -          if valid_const a T then None
   1.316 -          else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   1.317 -            quote (string_of_typ sg T))
   1.318 +        (case const_type sg a of
   1.319 +          None => Some ("Undeclared constant " ^ show_const a T)
   1.320 +        | Some U =>
   1.321 +            if Type.typ_instance (tsig, T, U) then None
   1.322 +            else Some ("Illegal type for constant " ^ show_const a T))
   1.323        | atom_err (Var ((x, i), _)) =
   1.324            if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   1.325        | atom_err _ = None;
   1.326 @@ -608,7 +610,7 @@
   1.327  
   1.328  fun infer_types sg def_type def_sort used freeze (ts, T) =
   1.329    let
   1.330 -    val Sg {tsig, ...} = sg;
   1.331 +    val tsig = tsig_of sg;
   1.332      val prt =
   1.333        setmp Syntax.show_brackets true
   1.334          (setmp long_names true (pretty_term sg));
   1.335 @@ -838,35 +840,34 @@
   1.336  
   1.337  (* the external interfaces *)
   1.338  
   1.339 -val add_classes      = extend_sign (ext_classes true) "#";
   1.340 -val add_classes_i    = extend_sign (ext_classes false) "#";
   1.341 -val add_classrel     = extend_sign (ext_classrel true) "#";
   1.342 -val add_classrel_i   = extend_sign (ext_classrel false) "#";
   1.343 -val add_defsort      = extend_sign (ext_defsort true) "#";
   1.344 -val add_defsort_i    = extend_sign (ext_defsort false) "#";
   1.345 -val add_types        = extend_sign ext_types "#";
   1.346 -val add_tyabbrs      = extend_sign ext_tyabbrs "#";
   1.347 -val add_tyabbrs_i    = extend_sign ext_tyabbrs_i "#";
   1.348 -val add_arities      = extend_sign (ext_arities true) "#";
   1.349 -val add_arities_i    = extend_sign (ext_arities false) "#";
   1.350 -val add_consts       = extend_sign ext_consts "#";
   1.351 -val add_consts_i     = extend_sign ext_consts_i "#";
   1.352 -val add_syntax       = extend_sign ext_syntax "#";
   1.353 -val add_syntax_i     = extend_sign ext_syntax_i "#";
   1.354 -val add_modesyntax   = extend_sign ext_modesyntax "#";
   1.355 -val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
   1.356 -val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
   1.357 -val add_trfunsT      = extend_sign (ext_syn Syntax.extend_trfunsT) "#";
   1.358 -val add_tokentrfuns  = extend_sign (ext_syn Syntax.extend_tokentrfuns) "#";
   1.359 -val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
   1.360 -val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
   1.361 -val add_path         = extend_sign ext_path "#";
   1.362 -val add_space        = extend_sign ext_space "#";
   1.363 -val init_data        = extend_sign ext_init_data "#";
   1.364 -val put_data         = extend_sign ext_put_data "#";
   1.365 -fun add_name name sg = extend_sign K name () sg;
   1.366 -
   1.367 -val make_draft = add_name "#";
   1.368 +val add_classes      = extend_sign true (ext_classes true) "#";
   1.369 +val add_classes_i    = extend_sign true (ext_classes false) "#";
   1.370 +val add_classrel     = extend_sign true (ext_classrel true) "#";
   1.371 +val add_classrel_i   = extend_sign true (ext_classrel false) "#";
   1.372 +val add_defsort      = extend_sign true (ext_defsort true) "#";
   1.373 +val add_defsort_i    = extend_sign true (ext_defsort false) "#";
   1.374 +val add_types        = extend_sign true ext_types "#";
   1.375 +val add_tyabbrs      = extend_sign true ext_tyabbrs "#";
   1.376 +val add_tyabbrs_i    = extend_sign true ext_tyabbrs_i "#";
   1.377 +val add_arities      = extend_sign true (ext_arities true) "#";
   1.378 +val add_arities_i    = extend_sign true (ext_arities false) "#";
   1.379 +val add_consts       = extend_sign true ext_consts "#";
   1.380 +val add_consts_i     = extend_sign true ext_consts_i "#";
   1.381 +val add_syntax       = extend_sign true ext_syntax "#";
   1.382 +val add_syntax_i     = extend_sign true ext_syntax_i "#";
   1.383 +val add_modesyntax   = extend_sign true ext_modesyntax "#";
   1.384 +val add_modesyntax_i = extend_sign true ext_modesyntax_i "#";
   1.385 +val add_trfuns       = extend_sign true (ext_syn Syntax.extend_trfuns) "#";
   1.386 +val add_trfunsT      = extend_sign true (ext_syn Syntax.extend_trfunsT) "#";
   1.387 +val add_tokentrfuns  = extend_sign true (ext_syn Syntax.extend_tokentrfuns) "#";
   1.388 +val add_trrules      = extend_sign true (ext_syn Syntax.extend_trrules) "#";
   1.389 +val add_trrules_i    = extend_sign true (ext_syn Syntax.extend_trrules_i) "#";
   1.390 +val add_path         = extend_sign true ext_path "#";
   1.391 +val add_space        = extend_sign true ext_space "#";
   1.392 +val init_data        = extend_sign true ext_init_data "#";
   1.393 +val put_data         = extend_sign true ext_put_data "#";
   1.394 +fun add_name name sg = extend_sign true K name () sg;
   1.395 +fun prep_ext sg      = extend_sign false K "#" () sg;
   1.396  
   1.397  
   1.398  
   1.399 @@ -895,18 +896,17 @@
   1.400    else
   1.401      (*neither is union already; must form union*)
   1.402      let
   1.403 -      val Sg {id = _, self = _, tsig = tsig1, const_tab = const_tab1, syn = syn1,
   1.404 -        path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1;
   1.405 -      val Sg {id = _, self = _, tsig = tsig2, const_tab = const_tab2, syn = syn2,
   1.406 -        path = _, spaces = spaces2, data = data2, stamps = stamps2} = sg2;
   1.407 -
   1.408 +      val Sg ({id = _, stamps = stamps1}, {self = _, tsig = tsig1, const_tab = const_tab1,
   1.409 +        syn = syn1, path = _, spaces = spaces1, data = data1}) = sg1;
   1.410 +      val Sg ({id = _, stamps = stamps2}, {self = _, tsig = tsig2, const_tab = const_tab2,
   1.411 +        syn = syn2, path = _, spaces = spaces2, data = data2}) = sg2;
   1.412  
   1.413        val id = ref "";
   1.414 -      val self_ref = ref sg1;			(*dummy value*)
   1.415 +      val self_ref = ref sg1;                   (*dummy value*)
   1.416        val self = SgRef (Some self_ref);
   1.417        val stamps = merge_rev_lists stamps1 stamps2;
   1.418        val _ =
   1.419 -        (case duplicates (stamp_names stamps) of
   1.420 +        (case duplicates (map ! stamps) of
   1.421            [] => ()
   1.422          | dups => raise TERM ("Attempt to merge different versions of theories "
   1.423              ^ commas_quote dups, []));