src/HOL/Tools/typedef_package.ML
changeset 5697 e816c4f1a396
parent 5180 d82a70766af0
child 6092 d9db67970c73
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Oct 20 16:36:40 1998 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Oct 20 16:37:02 1998 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature TYPEDEF_PACKAGE =
     1.6  sig
     1.7 +  val quiet_mode: bool ref
     1.8    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     1.9    val prove_nonempty: cterm -> thm list -> tactic option -> thm
    1.10    val add_typedef: string -> bstring * string list * mixfix ->
    1.11 @@ -39,6 +40,12 @@
    1.12  
    1.13  (** type definitions **)
    1.14  
    1.15 +(* messages *)
    1.16 +
    1.17 +val quiet_mode = ref false;
    1.18 +fun message s = if ! quiet_mode then () else writeln s;
    1.19 +
    1.20 +
    1.21  (* prove non-emptyness of a set *)   (*exception ERROR*)
    1.22  
    1.23  val is_def = Logic.is_equals o #prop o rep_thm;
    1.24 @@ -123,7 +130,7 @@
    1.25      if null errs then ()
    1.26      else error (cat_lines errs);
    1.27  
    1.28 -    writeln("Proving nonemptiness of " ^ quote name ^ " ...");
    1.29 +    message ("Proving nonemptiness of " ^ quote name ^ " ...");
    1.30      prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
    1.31  
    1.32      thy