1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 22 14:36:10 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Mon Feb 22 19:31:00 2010 +0100
     1.3 @@ -15,11 +15,9 @@
     1.4  exception FAIL
     1.5  
     1.6  (* int -> term -> string *)
     1.7 -fun minipick 0 _ = "none"
     1.8 -  | minipick n t =
     1.9 -    case minipick (n - 1) t of
    1.10 -      "none" => Minipick.pick_nits_in_term @{context} (K n) t
    1.11 -    | outcome_code => outcome_code
    1.12 +fun minipick n t =
    1.13 +  map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
    1.14 +  |> Minipick.solve_any_kodkod_problem @{theory}
    1.15  (* int -> term -> bool *)
    1.16  fun none n t = (minipick n t = "none" orelse raise FAIL)
    1.17  fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
    1.18 @@ -87,11 +85,11 @@
    1.19  ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    1.20  ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    1.21  ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    1.22 -ML {* none 8 @{prop "fst (a, b) = a"} *}
    1.23 +ML {* none 5 @{prop "fst (a, b) = a"} *}
    1.24  ML {* none 1 @{prop "fst (a, b) = b"} *}
    1.25  ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    1.26  ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    1.27 -ML {* none 8 @{prop "snd (a, b) = b"} *}
    1.28 +ML {* none 5 @{prop "snd (a, b) = b"} *}
    1.29  ML {* none 1 @{prop "snd (a, b) = a"} *}
    1.30  ML {* genuine 2 @{prop "snd (a, b) = a"} *}
    1.31  ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}