src/Pure/sorts.ML

   val insert_typs: typ list -> sort list -> sort list
   val insert_term: term -> sort list -> sort list
   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
   val class_less: algebra -> class * class -> bool
   val class_le: algebra -> class * class -> bool

      variable: typ -> ('a * class) list} ->
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
   val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
 end;
 
-structure Sorts : SORTS =
+structure Sorts: SORTS =
 struct
 
 
 (** ordered lists of sorts **)
 

     that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
     c1 <= c2 holds Ss1 <= Ss2.
 *)
 
 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;
 
 val classes_of = #classes o rep_algebra;

   error (cat_lines (map (fn cs =>
     "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
 
 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;
   in classes'' end);