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