--- 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