# HG changeset patch
# User wenzelm
# Date 908893554 -7200
# Node ID 1e5b4c66317ffd379df49243914393952d795026
# Parent  9a3acc4c7c2eb902caea41ea29468c0b11924e3d
quiet_mode, message;

diff -r 9a3acc4c7c2e -r 1e5b4c66317f src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Oct 20 16:25:14 1998 +0200
+++ b/src/Pure/axclass.ML	Tue Oct 20 16:25:54 1998 +0200
@@ -7,6 +7,7 @@
 
 signature AX_CLASS =
 sig
+  val quiet_mode: bool ref
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
   val add_axclass: bclass * xclass list -> (string * string) list
@@ -36,6 +37,12 @@
 
 (** utilities **)
 
+(* messages *)
+
+val quiet_mode = ref false;
+fun message s = if ! quiet_mode then () else writeln s;
+
+
 (* type vars *)
 
 fun map_typ_frees f (Type (t, tys)) = Type (t, map (map_typ_frees f) tys)
@@ -293,7 +300,7 @@
       if int then intrn_classrel (sign_of thy) raw_c1_c2
       else raw_c1_c2;
   in
-    writeln ("Proving class inclusion " ^
+    message ("Proving class inclusion " ^
       quote (Sign.str_of_classrel (sign_of thy) c1_c2) ^ " ...");
     add_classrel_thms
       [prove_subclass thy c1_c2 (witnesses thy names thms) usr_tac] thy
@@ -311,7 +318,7 @@
       else (raw_t, raw_Ss, raw_cs);
     val wthms = witnesses thy names thms;
     fun prove c =
-     (writeln ("Proving type arity " ^
+     (message ("Proving type arity " ^
         quote (Sign.str_of_arity sign (t, Ss, [c])) ^ " ...");
         prove_arity thy (t, Ss, c) wthms usr_tac);
   in