make Nitpick's unsound mode a bit more unsound
authorblanchet
Mon, 21 Jun 2010 16:59:37 +0200
changeset 37483 4de0b0c38bdf
parent 37482 6849464ab10e
child 37484 b7821e89fb79
child 37486 b993fac7985b
make Nitpick's unsound mode a bit more unsound
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)