# HG changeset patch
# User wenzelm
# Date 876757790 -7200
# Node ID 4bdf32173f6ff2947912b4cc544599d218c9cf57
# Parent  762606a888fe2b539a56d19cc6962b0c2dd91b75
fixed extern;
added str_of_classrel, str_of_arity, str_of_arity;

diff -r 762606a888fe -r 4bdf32173f6f src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Oct 13 17:49:08 1997 +0200
+++ b/src/Pure/sign.ML	Mon Oct 13 17:49:50 1997 +0200
@@ -59,6 +59,9 @@
   val string_of_term: sg -> term -> string
   val string_of_typ: sg -> typ -> string
   val string_of_sort: sg -> sort -> string
+  val str_of_sort: sg -> sort -> string
+  val str_of_classrel: sg -> class * class -> string
+  val str_of_arity: sg -> string * sort list * sort -> string
   val pprint_term: sg -> term -> pprint_args -> unit
   val pprint_typ: sg -> typ -> pprint_args -> unit
   val certify_typ: sg -> typ -> typ
@@ -287,7 +290,7 @@
     map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;
 
   val intern = intrn o spaces_of;
-  val extern = intrn o spaces_of;
+  val extern = extrn o spaces_of;
   val intern_class = intrn_class o spaces_of;
   val extern_class = extrn_class o spaces_of;
   val intern_sort = intrn_sort o spaces_of;
@@ -388,11 +391,24 @@
   Syntax.pretty_sort syn
     (if ! long_names then S else extrn_sort spaces S);
 
+fun pretty_classrel sg (c1, c2) = Pretty.block
+  [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
+
+fun pretty_arity sg (t, [], S) = Pretty.block
+      [Pretty.str (t ^ " ::"), Pretty.brk 1, pretty_sort sg S]
+  | pretty_arity sg (t, Ss, S) = Pretty.block
+      [Pretty.str (t ^ " ::"), Pretty.brk 1,
+        Pretty.list "(" ")" (map (pretty_sort sg) Ss),
+        Pretty.brk 1, pretty_sort sg S];
 
 fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
 fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);
 fun string_of_sort sg S = Pretty.string_of (pretty_sort sg S);
 
+fun str_of_sort sg S = Pretty.str_of (pretty_sort sg S);
+fun str_of_classrel sg c1_c2 = Pretty.str_of (pretty_classrel sg c1_c2);
+fun str_of_arity sg ar = Pretty.str_of (pretty_arity sg ar);
+
 fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
 fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);