src/HOL/Tools/Nitpick/nitpick.ML
changeset 33955 fff6f11b1f09
parent 33877 e779bea3d337
child 33982 1ae222745c4a
--- 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