serial numbers for types;
authorwenzelm
Thu Sep 21 19:05:41 2006 +0200 (2006-09-21 ago)
changeset 2067493baed0f741c
parent 20673 27738ccd0700
child 20675 cb19d18aef01
serial numbers for types;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Thu Sep 21 19:05:31 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Sep 21 19:05:41 2006 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val rep_tsig: tsig ->
     1.5     {classes: NameSpace.T * Sorts.algebra,
     1.6      default: sort,
     1.7 -    types: (decl * stamp) NameSpace.table,
     1.8 +    types: (decl * serial) NameSpace.table,
     1.9      log_types: string list,
    1.10      witness: (typ * sort) option}
    1.11    val empty_tsig: tsig
    1.12 @@ -99,7 +99,7 @@
    1.13    TSig of {
    1.14      classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
    1.15      default: sort,                          (*default sort on input*)
    1.16 -    types: (decl * stamp) NameSpace.table,  (*declared types*)
    1.17 +    types: (decl * serial) NameSpace.table, (*declared types*)
    1.18      log_types: string list,                 (*logical types sorted by number of arguments*)
    1.19      witness: (typ * sort) option};          (*witness for non-emptiness of strictest sort*)
    1.20  
    1.21 @@ -527,7 +527,7 @@
    1.22      val types' =
    1.23        (case Symtab.lookup types c' of
    1.24          SOME (decl', _) => err_in_decls c' decl decl'
    1.25 -      | NONE => Symtab.update (c', (decl, stamp ())) types);
    1.26 +      | NONE => Symtab.update (c', (decl, serial ())) types);
    1.27    in (space', types') end;
    1.28  
    1.29  fun the_decl (_, types) = fst o the o Symtab.lookup types;
    1.30 @@ -568,8 +568,8 @@
    1.31  fun add_nonterminals naming = map_types o fold (new_decl naming) o map (rpair Nonterminal);
    1.32  
    1.33  fun merge_types (types1, types2) =
    1.34 -  NameSpace.merge_tables (Library.eq_snd (op =)) (types1, types2) handle Symtab.DUPS (d :: _) =>
    1.35 -    err_in_decls d (the_decl types1 d) (the_decl types2 d);
    1.36 +  NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)
    1.37 +    handle Symtab.DUPS (d :: _) => err_in_decls d (the_decl types1 d) (the_decl types2 d);
    1.38  
    1.39  end;
    1.40