src/HOL/Tools/sat_solver.ML
changeset 33037 b22e44496dc2
parent 32952 aeb1e44fbc19
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -471,8 +471,8 @@
     1.4          | forced_vars False             = []
     1.5          | forced_vars (BoolVar i)       = [i]
     1.6          | forced_vars (Not (BoolVar i)) = [~i]
     1.7 -        | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
     1.8 -        | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
     1.9 +        | forced_vars (Or (fm1, fm2))   = gen_inter (op =) (forced_vars fm1, forced_vars fm2)
    1.10 +        | forced_vars (And (fm1, fm2))  = gen_union (op =) (forced_vars fm1, forced_vars fm2)
    1.11          (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
    1.12          (* precedence, and the next partial evaluation of the formula returns 'False'. *)
    1.13          | forced_vars _                 = error "formula is not in negation normal form"