# HG changeset patch
# User wenzelm
# Date 1085835652 -7200
# Node ID 336ade035a34ae8aa15f0839986f6b66079eb4bf
# Parent  ebb8499d0fd2c86577e6db7a0dfe1b8535e99fba
improved output;

diff -r ebb8499d0fd2 -r 336ade035a34 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat May 29 15:00:25 2004 +0200
+++ b/src/Pure/axclass.ML	Sat May 29 15:00:52 2004 +0200
@@ -349,11 +349,11 @@
     handle ERROR => error ("The error(s) above occurred while trying to prove " ^
      quote (str_of sign prop))) |> Drule.standard;
 
-val prove_subclass =
-  prove mk_classrel (fn sg => fn c1_c2 => Sign.str_of_classrel sg c1_c2);
+val prove_subclass = prove mk_classrel (fn sg => fn (c1, c2) =>
+  Pretty.string_of_classrel (Sign.pp sg) [c1, c2]);
 
-val prove_arity =
-  prove mk_arity (fn sg => fn (t, Ss, c) => Sign.str_of_arity sg (t, Ss, [c]));
+val prove_arity = prove mk_arity (fn sg => fn (t, Ss, c) =>
+  Pretty.string_of_arity (Sign.pp sg) (t, Ss, [c]));
 
 
 
@@ -363,14 +363,14 @@
 
 fun read_class sg c = Sign.certify_class sg (Sign.intern_class sg c);
 
-fun test_classrel sg cc = (Type.add_classrel [cc] (Sign.tsig_of sg); cc);
+fun test_classrel sg cc = (Type.add_classrel (Sign.pp sg) [cc] (Sign.tsig_of sg); cc);
 fun cert_classrel sg = test_classrel sg o Library.pairself (Sign.certify_class sg);
 fun read_classrel sg = test_classrel sg o Library.pairself (read_class sg);
 
-fun test_arity sg ar = (Type.add_arities [ar] (Sign.tsig_of sg); ar);
+fun test_arity sg ar = (Type.add_arities (Sign.pp sg) [ar] (Sign.tsig_of sg); ar);
 
 fun prep_arity prep_tycon prep_sort prep_x sg (t, Ss, x) =
-  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);  
+  test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep_x sg x);
 
 val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
 val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
@@ -381,10 +381,10 @@
 fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
   let
     val sign = Theory.sign_of thy;
-    val c1_c2 = prep_classrel sign raw_c1_c2;
+    val (c1, c2) = prep_classrel sign raw_c1_c2;
   in
-    message ("Proving class inclusion " ^ quote (Sign.str_of_classrel sign c1_c2) ^ " ...");
-    thy |> add_classrel_thms [prove_subclass sign c1_c2 (witnesses thy names thms) usr_tac]
+    message ("Proving class inclusion " ^ quote (Sign.string_of_classrel sign [c1, c2]) ^ " ...");
+    thy |> add_classrel_thms [prove_subclass sign (c1, c2) (witnesses thy names thms) usr_tac]
   end;
 
 fun ext_inst_arity prep_arity (raw_t, raw_Ss, raw_cs) names thms usr_tac thy =
@@ -394,7 +394,7 @@
     val wthms = witnesses thy names thms;
     fun prove c =
      (message ("Proving type arity " ^
-        quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ...");
+        quote (Sign.string_of_arity sign (t, Ss, [c])) ^ " ...");
         prove_arity sign (t, Ss, c) wthms usr_tac);
   in add_arity_thms (map prove cs) thy end;
 
diff -r ebb8499d0fd2 -r 336ade035a34 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat May 29 15:00:25 2004 +0200
+++ b/src/Pure/drule.ML	Sat May 29 15:00:52 2004 +0200
@@ -297,7 +297,7 @@
 (*Strip extraneous shyps as far as possible*)
 fun strip_shyps_warning thm =
   let
-    val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm);
+    val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.sign_of_thm thm);
     val thm' = Thm.strip_shyps thm;
     val xshyps = Thm.extra_shyps thm';
   in