# HG changeset patch
# User krauss
# Date 1233583938 -3600
# Node ID 944657d6932ea0e7ec10765386deaebb80b12495
# Parent  64d41ad4ffc2416fc87b2238473366361cf61467
fix potential incompleteness in SAT encoding

diff -r 64d41ad4ffc2 -r 944657d6932e src/HOL/Tools/function_package/scnp_solve.ML
--- a/src/HOL/Tools/function_package/scnp_solve.ML	Mon Feb 02 13:56:24 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_solve.ML	Mon Feb 02 15:12:18 2009 +0100
@@ -151,33 +151,33 @@
     val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
 
     fun encode_graph MAX (g, p, q, n, m, _) =
-        all [
+        And (
           Equiv (WEAK g,
             iforall m (fn j =>
               Implies (P (q, j),
                 iexists n (fn i =>
                   And (P (p, i), EW (g, i, j)))))),
           Equiv (STRICT g,
-            iforall m (fn j =>
-              Implies (P (q, j),
-                iexists n (fn i =>
-                  And (P (p, i), ES (g, i, j)))))),
-          iexists n (fn i => P (p, i))
-        ]
+            And (
+              iforall m (fn j =>
+                Implies (P (q, j),
+                  iexists n (fn i =>
+                    And (P (p, i), ES (g, i, j))))),
+              iexists n (fn i => P (p, i)))))
       | encode_graph MIN (g, p, q, n, m, _) =
-        all [
+        And (
           Equiv (WEAK g,
             iforall n (fn i =>
               Implies (P (p, i),
                 iexists m (fn j =>
                   And (P (q, j), EW (g, i, j)))))),
           Equiv (STRICT g,
-            iforall n (fn i =>
-              Implies (P (p, i),
-                iexists m (fn j =>
-                  And (P (q, j), ES (g, i, j)))))),
-          iexists m (fn j => P (q, j))
-        ]
+            And (
+              iforall n (fn i =>
+                Implies (P (p, i),
+                  iexists m (fn j =>
+                    And (P (q, j), ES (g, i, j))))),
+              iexists m (fn j => P (q, j)))))
       | encode_graph MS (g, p, q, n, m, _) =
         all [
           Equiv (WEAK g,