# HG changeset patch
# User wenzelm
# Date 870872873 -7200
# Node ID 1884b433c6a526723c40bc0e4b286ae7b9e0d43c
# Parent  17527284f100e71f28004f3d3001ca9f330b1949
added str_of_classrel;

diff -r 17527284f100 -r 1884b433c6a5 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Wed Aug 06 15:07:33 1997 +0200
+++ b/src/Pure/sorts.ML	Wed Aug 06 15:07:53 1997 +0200
@@ -9,6 +9,7 @@
 sig
   type classrel
   type arities
+  val str_of_classrel: class * class -> string
   val str_of_sort: sort -> string
   val str_of_arity: string * sort list * sort -> string
   val class_eq: classrel -> class * class -> bool
@@ -64,6 +65,8 @@
 
 (* print sorts and arities *)
 
+fun str_of_classrel (c1, c2) = c1 ^ " < " ^ c2;
+
 fun str_of_sort [c] = c
   | str_of_sort cs = enclose "{" "}" (commas cs);