1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 26 16:50:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 26 18:38:23 2010 +0100
     1.3 @@ -1451,9 +1451,10 @@
     1.4             @{const Not} $ (is_unknown_t $ normal_y),
     1.5             equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
     1.6             Logic.mk_equals (normal_x, normal_y)),
     1.7 -     @{const "==>"}
     1.8 -         $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
     1.9 -         $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
    1.10 +     Logic.list_implies
    1.11 +         ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)),
    1.12 +           HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))],
    1.13 +          HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
    1.14    end
    1.15  
    1.16  (* theory -> (typ option * bool) list -> int * styp -> term *)

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 26 16:50:09 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 26 18:38:23 2010 +0100
     2.3 @@ -281,7 +281,7 @@
     2.4               js 0
     2.5        end
     2.6      (* bool -> typ -> typ -> (term * term) list -> term *)
     2.7 -    fun make_set maybe_opt T1 T2 =
     2.8 +    fun make_set maybe_opt T1 T2 tps =
     2.9        let
    2.10          val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
    2.11          val insert_const = Const (@{const_name insert},
    2.12 @@ -293,13 +293,20 @@
    2.13              else
    2.14                empty_const
    2.15            | aux ((t1, t2) :: zs) =
    2.16 -            aux zs |> t2 <> @{const False}
    2.17 -                      ? curry (op $) (insert_const
    2.18 -                                      $ (t1 |> t2 <> @{const True}
    2.19 -                                               ? curry (op $)
    2.20 -                                                       (Const (maybe_name,
    2.21 -                                                               T1 --> T1))))
    2.22 -      in aux end
    2.23 +            aux zs
    2.24 +            |> t2 <> @{const False}
    2.25 +               ? curry (op $)
    2.26 +                       (insert_const
    2.27 +                        $ (t1 |> t2 <> @{const True}
    2.28 +                                 ? curry (op $)
    2.29 +                                         (Const (maybe_name, T1 --> T1))))
    2.30 +      in
    2.31 +        if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
    2.32 +                  tps then
    2.33 +          Const (unknown, T1 --> T2)
    2.34 +        else
    2.35 +          aux tps
    2.36 +      end
    2.37      (* typ -> typ -> typ -> (term * term) list -> term *)
    2.38      fun make_map T1 T2 T2' =
    2.39        let

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Feb 26 16:50:09 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Feb 26 18:38:23 2010 +0100
     3.3 @@ -19,9 +19,7 @@
     3.4  open Nitpick_Nut
     3.5  open Nitpick_Kodkod
     3.6  
     3.7 -val settings =
     3.8 -  [("solver", "\"zChaff\""),
     3.9 -   ("skolem_depth", "-1")]
    3.10 +val settings = [("solver", "\"DefaultSAT4J\"")]
    3.11  
    3.12  fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)
    3.13