--- a/src/HOL/Nominal/nominal_primrec.ML Sat Mar 29 13:03:05 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sat Mar 29 13:03:07 2008 +0100
@@ -8,7 +8,6 @@
signature NOMINAL_PRIMREC =
sig
- val quiet_mode: bool ref
val add_primrec: string -> string list option -> string option ->
((bstring * string) * Attrib.src list) list -> theory -> Proof.state
val add_primrec_unchecked: string -> string list option -> string option ->
@@ -31,12 +30,6 @@
primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
(* preprocessing of equations *)
fun process_eqn thy eq rec_fns =