src/Pure/sorts.ML
changeset 3633 1884b433c6a5
parent 2990 271062b8c461
child 3783 37fb4f64eb9d
     1.1 --- a/src/Pure/sorts.ML	Wed Aug 06 15:07:33 1997 +0200
     1.2 +++ b/src/Pure/sorts.ML	Wed Aug 06 15:07:53 1997 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    type classrel
     1.6    type arities
     1.7 +  val str_of_classrel: class * class -> string
     1.8    val str_of_sort: sort -> string
     1.9    val str_of_arity: string * sort list * sort -> string
    1.10    val class_eq: classrel -> class * class -> bool
    1.11 @@ -64,6 +65,8 @@
    1.12  
    1.13  (* print sorts and arities *)
    1.14  
    1.15 +fun str_of_classrel (c1, c2) = c1 ^ " < " ^ c2;
    1.16 +
    1.17  fun str_of_sort [c] = c
    1.18    | str_of_sort cs = enclose "{" "}" (commas cs);
    1.19