# HG changeset patch
# User blanchet
# Date 1277132377 -7200
# Node ID 4de0b0c38bdfa1fb6f0ebd3fcb45f94c305776e7
# Parent  6849464ab10eb2dbac6320f0d73139ee94366b4a
make Nitpick's unsound mode a bit more unsound

diff -r 6849464ab10e -r 4de0b0c38bdf src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Jun 21 14:07:00 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Jun 21 16:59:37 2010 +0200
@@ -874,7 +874,7 @@
           end
         | Cst (cst, T, _) =>
           if cst = Unknown orelse cst = Unrep then
-            case (is_boolean_type T, polar) of
+            case (is_boolean_type T, polar |> unsound ? flip_polarity) of
               (true, Pos) => Cst (False, T, Formula Pos)
             | (true, Neg) => Cst (True, T, Formula Neg)
             | _ => Cst (cst, T, best_opt_set_rep_for_type scope T)