diff -r 6a5986170c1d -r 0819931d652d src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 17 18:18:27 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 17 22:54:38 2014 +0100
@@ -1059,8 +1059,8 @@
 (* Give the inner timeout a chance. *)
 val timeout_bonus = seconds 1.0
 
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
-                      step subst def_assm_ts nondef_assm_ts orig_t =
+fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
+                      subst def_assm_ts nondef_assm_ts orig_t =
   let
     val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
     val print_t = if mode = TPTP then Output.urgent_message else K ()