src/HOL/Tools/sat_solver.ML
changeset 14703 837d7180c39a
parent 14514 15abb7d42e2e
child 14753 f40b45db8cf0
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue May 04 11:25:08 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue May 04 18:04:28 2004 +0200
     1.3 @@ -299,7 +299,6 @@
     1.4  			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
     1.5  			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
     1.6  			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
     1.7 -			  | partial_eval xs _                = raise ERROR  (* formula is not in negation normal form *)
     1.8  			(* prop_formula -> int list *)
     1.9  			fun forced_vars True              = []
    1.10  			  | forced_vars False             = []