--- a/src/ZF/Tools/inductive_package.ML Sat Dec 30 12:41:59 2006 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Dec 30 16:08:00 2006 +0100
@@ -148,8 +148,10 @@
val big_rec_name = Sign.intern_const thy big_rec_base_name;
- val dummy = conditional verbose (fn () =>
- writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
+ val _ =
+ if verbose then
+ writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)
+ else ();
(*Forbid the inductive definition structure from clashing with a theory
name. This restriction may become obsolete as ML is de-emphasized.*)