--- a/src/HOL/Tools/sat_solver.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML Tue Oct 20 16:13:01 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)) = gen_inter (op =) (forced_vars fm1, forced_vars fm2)
+ | forced_vars (And (fm1, fm2)) = gen_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"