# HG changeset patch
# User blanchet
# Date 1267205903 -3600
# Node ID 42d39948cace08bcc9f677c0cfde6fc15f69c3b9
# Parent  4356263e0bdd794d6a89bacf830567e952515e66
use SAT4J for "Tests_Nits.thy" for safety (this should solve the Isatest failures) + minor changes

diff -r 4356263e0bdd -r 42d39948cace src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 26 16:50:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 26 18:38:23 2010 +0100
@@ -1451,9 +1451,10 @@
            @{const Not} $ (is_unknown_t $ normal_y),
            equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
            Logic.mk_equals (normal_x, normal_y)),
-     @{const "==>"}
-         $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
-         $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
+     Logic.list_implies
+         ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)),
+           HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))],
+          HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
   end
 
 (* theory -> (typ option * bool) list -> int * styp -> term *)
diff -r 4356263e0bdd -r 42d39948cace src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 26 16:50:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 26 18:38:23 2010 +0100
@@ -281,7 +281,7 @@
              js 0
       end
     (* bool -> typ -> typ -> (term * term) list -> term *)
-    fun make_set maybe_opt T1 T2 =
+    fun make_set maybe_opt T1 T2 tps =
       let
         val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
         val insert_const = Const (@{const_name insert},
@@ -293,13 +293,20 @@
             else
               empty_const
           | aux ((t1, t2) :: zs) =
-            aux zs |> t2 <> @{const False}
-                      ? curry (op $) (insert_const
-                                      $ (t1 |> t2 <> @{const True}
-                                               ? curry (op $)
-                                                       (Const (maybe_name,
-                                                               T1 --> T1))))
-      in aux end
+            aux zs
+            |> t2 <> @{const False}
+               ? curry (op $)
+                       (insert_const
+                        $ (t1 |> t2 <> @{const True}
+                                 ? curry (op $)
+                                         (Const (maybe_name, T1 --> T1))))
+      in
+        if forall (fn (_, t) => t <> @{const True} andalso t <> @{const False})
+                  tps then
+          Const (unknown, T1 --> T2)
+        else
+          aux tps
+      end
     (* typ -> typ -> typ -> (term * term) list -> term *)
     fun make_map T1 T2 T2' =
       let
diff -r 4356263e0bdd -r 42d39948cace src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Feb 26 16:50:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Feb 26 18:38:23 2010 +0100
@@ -19,9 +19,7 @@
 open Nitpick_Nut
 open Nitpick_Kodkod
 
-val settings =
-  [("solver", "\"zChaff\""),
-   ("skolem_depth", "-1")]
+val settings = [("solver", "\"DefaultSAT4J\"")]
 
 fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)