diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 24 14:37:23 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 24 17:28:25 2009 +0100 @@ -655,7 +655,7 @@ update_checked_problems problems (unsat_js @ map fst lib_ps); if null con_ps then let - val num_genuine = Library.take (max_potential, lib_ps) + val num_genuine = take max_potential lib_ps |> map (print_and_check false) |> filter (equal (SOME true)) |> length val max_genuine = max_genuine - num_genuine @@ -689,7 +689,7 @@ end else let - val _ = Library.take (max_genuine, con_ps) + val _ = take max_genuine con_ps |> List.app (ignore o print_and_check true) val max_genuine = max_genuine - length con_ps in