quiet_mode, message;

--- a/src/HOL/Tools/typedef_package.ML	Tue Oct 20 16:36:40 1998 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Oct 20 16:37:02 1998 +0200
@@ -7,6 +7,7 @@
 
 signature TYPEDEF_PACKAGE =
 sig
+  val quiet_mode: bool ref
   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   val prove_nonempty: cterm -> thm list -> tactic option -> thm
   val add_typedef: string -> bstring * string list * mixfix ->
@@ -39,6 +40,12 @@
 
 (** type definitions **)
 
+(* messages *)
+
+val quiet_mode = ref false;
+fun message s = if ! quiet_mode then () else writeln s;
+
+
 (* prove non-emptyness of a set *)   (*exception ERROR*)
 
 val is_def = Logic.is_equals o #prop o rep_thm;
@@ -123,7 +130,7 @@
     if null errs then ()
     else error (cat_lines errs);
 
-    writeln("Proving nonemptiness of " ^ quote name ^ " ...");
+    message ("Proving nonemptiness of " ^ quote name ^ " ...");
     prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
 
     thy