src/Pure/sorts.ML
changeset 20573 c945a208e7f8
parent 20465 95f6d354b0ed
child 21926 1091904ddb19
     1.1 --- a/src/Pure/sorts.ML	Mon Sep 18 19:12:44 2006 +0200
     1.2 +++ b/src/Pure/sorts.ML	Mon Sep 18 19:12:45 2006 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    val insert_terms: term list -> sort list -> sort list
     1.5    type algebra
     1.6    val rep_algebra: algebra ->
     1.7 -   {classes: stamp Graph.T,
     1.8 +   {classes: serial Graph.T,
     1.9      arities: (class * (class * sort list)) list Symtab.table}
    1.10    val classes: algebra -> class list
    1.11    val super_classes: algebra -> class -> class list
    1.12 @@ -57,7 +57,7 @@
    1.13    val witness_sorts: algebra -> string list -> sort list -> sort list -> (typ * sort) list
    1.14  end;
    1.15  
    1.16 -structure Sorts : SORTS =
    1.17 +structure Sorts: SORTS =
    1.18  struct
    1.19  
    1.20  
    1.21 @@ -103,7 +103,7 @@
    1.22  *)
    1.23  
    1.24  datatype algebra = Algebra of
    1.25 - {classes: stamp Graph.T,
    1.26 + {classes: serial Graph.T,
    1.27    arities: (class * (class * sort list)) list Symtab.table};
    1.28  
    1.29  fun rep_algebra (Algebra args) = args;
    1.30 @@ -189,7 +189,7 @@
    1.31  
    1.32  fun add_class pp (c, cs) = map_classes (fn classes =>
    1.33    let
    1.34 -    val classes' = classes |> Graph.new_node (c, stamp ())
    1.35 +    val classes' = classes |> Graph.new_node (c, serial ())
    1.36        handle Graph.DUP dup => err_dup_classes [dup];
    1.37      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
    1.38        handle Graph.CYCLES css => err_cyclic_classes pp css;