# HG changeset patch
# User blanchet
# Date 1280752040 -7200
# Node ID bc546396b818810e462d4490ebbaeee17b76af59
# Parent  824e940a3dd0bdfe52a0b338d9c6d021dda03f8a
prefer implication to equality, to be more SAT solver friendly

diff -r 824e940a3dd0 -r bc546396b818 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 13:48:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 02 14:27:20 2010 +0200
@@ -1866,11 +1866,11 @@
           |> foldr1 s_conj
       in List.foldr absdummy core_t arg_Ts end
   in
-    [HOLogic.eq_const bool_T $ (bisim_const T $ n_var $ x_var $ y_var)
-     $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
-        $ (s_betapply []
-                      (optimized_case_def hol_ctxt T bool_T (map case_func xs),
-                       x_var))),
+    [HOLogic.mk_imp
+       (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
+            s_betapply [] (optimized_case_def hol_ctxt T bool_T
+                                              (map case_func xs), x_var)),
+        bisim_const T $ n_var $ x_var $ y_var),
      HOLogic.eq_const set_T $ (bisim_const T $ bisim_max $ x_var)
      $ (Const (@{const_name insert}, T --> set_T --> set_T)
         $ x_var $ Const (@{const_name bot_class.bot}, set_T))]