1.1 --- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -638,22 +638,22 @@
     1.4      | SOME results =>
     1.5          let
     1.6            val msg = pretty_counterex_and_reports ctxt auto results
     1.7 -                    |> not auto ? tap (Output.urgent_message o Pretty.string_of)
     1.8          in
     1.9            if exists found_counterexample results then
    1.10              (genuineN,
    1.11 -             state |> (if auto then
    1.12 -                         Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    1.13 -                             Pretty.mark Markup.hilite msg]))
    1.14 -                       else
    1.15 -                         I))
    1.16 +             state
    1.17 +             |> (if auto then
    1.18 +                   Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    1.19 +                       Pretty.mark Markup.hilite msg]))
    1.20 +                 else
    1.21 +                   tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
    1.22            else
    1.23              (noneN, state)
    1.24          end
    1.25    end
    1.26    |> `(fn (outcome_code, _) => outcome_code = genuineN)
    1.27  
    1.28 -val setup = Try.register_tool (quickcheckN, (30, auto, try_quickcheck))
    1.29 +val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck))
    1.30  
    1.31  end;
    1.32