src/HOL/Tools/Nitpick/nitpick.ML
changeset 55539 0819931d652d
parent 54816 10d48c2a3e32
child 55888 cac1add157e8
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 17 18:18:27 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 17 22:54:38 2014 +0100
     1.3 @@ -1059,8 +1059,8 @@
     1.4  (* Give the inner timeout a chance. *)
     1.5  val timeout_bonus = seconds 1.0
     1.6  
     1.7 -fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
     1.8 -                      step subst def_assm_ts nondef_assm_ts orig_t =
     1.9 +fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
    1.10 +                      subst def_assm_ts nondef_assm_ts orig_t =
    1.11    let
    1.12      val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
    1.13      val print_t = if mode = TPTP then Output.urgent_message else K ()