# HG changeset patch
# User wenzelm
# Date 876757748 -7200
# Node ID 762606a888fe2b539a56d19cc6962b0c2dd91b75
# Parent  73c074f41749081bf4c106a704d7347f67e362b8
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;

diff -r 73c074f41749 -r 762606a888fe src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Oct 13 17:47:59 1997 +0200
+++ b/src/Pure/axclass.ML	Mon Oct 13 17:49:08 1997 +0200
@@ -271,13 +271,13 @@
     prove_goalw_cterm [] goal (K [tac])
   end
   handle ERROR => error ("The error(s) above occurred while trying to prove "
-    ^ quote (str_of sig_prop));
+    ^ quote (str_of (sign_of thy, sig_prop)));
 
 val prove_subclass =
-  prove mk_classrel (fn (c1, c2) => c1 ^ " < " ^ c2);
+  prove mk_classrel (fn (sg, c1_c2) => Sign.str_of_classrel sg c1_c2);
 
 val prove_arity =
-  prove mk_arity (fn (t, ss, c) => Sorts.str_of_arity (t, ss, [c]));
+  prove mk_arity (fn (sg, (t, Ss, c)) => Sign.str_of_arity sg (t, Ss, [c]));
 
 
 (* make goals (for interactive use) *)
@@ -297,7 +297,8 @@
     val intrn = if int then pairself (Sign.intern_class (sign_of thy)) else I;
     val c1_c2 = intrn raw_c1_c2;
   in
-    writeln ("Proving class inclusion " ^ quote (Sorts.str_of_classrel c1_c2) ^ " ...");
+    writeln ("Proving class inclusion " ^
+      quote (Sign.str_of_classrel (sign_of thy) c1_c2) ^ " ...");
     add_classrel_thms
       [prove_subclass thy c1_c2 (witnesses thy axms thms) usr_tac] thy
   end;
@@ -314,8 +315,9 @@
       else (raw_t, raw_Ss, raw_cs);
     val wthms = witnesses thy axms thms;
     fun prove c =
-     (writeln ("Proving type arity " ^ quote (Sorts.str_of_arity (t, Ss, [c])) ^ " ...");
-      prove_arity thy (t, Ss, c) wthms usr_tac);
+     (writeln ("Proving type arity " ^
+        quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ...");
+        prove_arity thy (t, Ss, c) wthms usr_tac);
   in
     add_arity_thms (map prove cs) thy
   end;