# HG changeset patch
# User wenzelm
# Date 1158599565 -7200
# Node ID c945a208e7f8a9e8021504f8f0866ebd88e8840a
# Parent  2b88de40da576b810ac3cf52a1e902ef758b3a99
classes: maintain serial number;

diff -r 2b88de40da57 -r c945a208e7f8 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Sep 18 19:12:44 2006 +0200
+++ b/src/Pure/sorts.ML	Mon Sep 18 19:12:45 2006 +0200
@@ -26,7 +26,7 @@
   val insert_terms: term list -> sort list -> sort list
   type algebra
   val rep_algebra: algebra ->
-   {classes: stamp Graph.T,
+   {classes: serial Graph.T,
     arities: (class * (class * sort list)) list Symtab.table}
   val classes: algebra -> class list
   val super_classes: algebra -> class -> class list
@@ -57,7 +57,7 @@
   val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
 end;
 
-structure Sorts : SORTS =
+structure Sorts: SORTS =
 struct
 
 
@@ -103,7 +103,7 @@
 *)
 
 datatype algebra = Algebra of
- {classes: stamp Graph.T,
+ {classes: serial Graph.T,
   arities: (class * (class * sort list)) list Symtab.table};
 
 fun rep_algebra (Algebra args) = args;
@@ -189,7 +189,7 @@
 
 fun add_class pp (c, cs) = map_classes (fn classes =>
   let
-    val classes' = classes |> Graph.new_node (c, stamp ())
+    val classes' = classes |> Graph.new_node (c, serial ())
       handle Graph.DUP dup => err_dup_classes [dup];
     val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
       handle Graph.CYCLES css => err_cyclic_classes pp css;