1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 24 14:37:23 2009 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Nov 24 17:28:25 2009 +0100
1.3 @@ -655,7 +655,7 @@
1.4 update_checked_problems problems (unsat_js @ map fst lib_ps);
1.5 if null con_ps then
1.6 let
1.7 - val num_genuine = Library.take (max_potential, lib_ps)
1.8 + val num_genuine = take max_potential lib_ps
1.9 |> map (print_and_check false)
1.10 |> filter (equal (SOME true)) |> length
1.11 val max_genuine = max_genuine - num_genuine
1.12 @@ -689,7 +689,7 @@
1.13 end
1.14 else
1.15 let
1.16 - val _ = Library.take (max_genuine, con_ps)
1.17 + val _ = take max_genuine con_ps
1.18 |> List.app (ignore o print_and_check true)
1.19 val max_genuine = max_genuine - length con_ps
1.20 in