Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/sat_solver.ML
changeset 33050 fe166e8b9f07
parent 33042 ddf1f03a9ad9
parent 33049 c38f02fdf35d
child 33228 cf8da4f3f92b 
--- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:08:52 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 12:12:21 2009 +0200
@@ -471,7 +471,7 @@
         | forced_vars False             = []
         | forced_vars (BoolVar i)       = [i]
         | forced_vars (Not (BoolVar i)) = [~i]
-        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1, forced_vars fm2)
+        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1) (forced_vars fm2)
         | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1) (forced_vars fm2)
         (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
         (* precedence, and the next partial evaluation of the formula returns 'False'. *)
isabelle