# HG changeset patch
# User wenzelm
# Date 1206792187 -3600
# Node ID 4e78281b32735056f55022791fd9c37fde090e79
# Parent  3cc1e48d0ce19b638d01c3ecc42d2b161a72627c
eliminated quiete_mode ref (unused);

diff -r 3cc1e48d0ce1 -r 4e78281b3273 src/HOL/Nominal/nominal_primrec.ML
--- 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 =