diff -r c61fe520602b -r 5018f6a76b3f src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 08:16:25 2009 +0200
@@ -471,8 +471,8 @@
         | forced_vars False             = []
         | forced_vars (BoolVar i)       = [i]
         | forced_vars (Not (BoolVar i)) = [~i]
-        | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
-        | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (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'. *)
         | forced_vars _                 = error "formula is not in negation normal form"