# HG changeset patch
# User blanchet
# Date 1273831276 -7200
# Node ID 55b97cb3806e5875f9459081b00e80cb76537429
# Parent  0e2818493775fbbd44d5aead545d86da06943572
produce more potential counterexamples for subset operator (cf. quantifiers)

diff -r 0e2818493775 -r 55b97cb3806e src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri May 14 11:24:49 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Fri May 14 12:01:16 2010 +0200
@@ -970,11 +970,11 @@
           in
             if is_opt_rep R then
               triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
-            else if opt andalso polar = Pos andalso
-                    not (is_concrete_type datatypes true (type_of u1)) then
+            else if not opt orelse unsound orelse polar = Neg orelse
+                    is_concrete_type datatypes true (type_of u1) then
+              s_op2 Subset T R u1 u2
+            else
               Cst (False, T, Formula Pos)
-            else
-              s_op2 Subset T R u1 u2
           end
         | Op2 (DefEq, T, _, u1, u2) =>
           s_op2 DefEq T (Formula Neut) (sub u1) (sub u2)