diff -r 64844b4cc107 -r 837d7180c39a src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Tue May 04 11:25:08 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Tue May 04 18:04:28 2004 +0200
@@ -299,7 +299,6 @@
 			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
 			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
 			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
-			  | partial_eval xs _                = raise ERROR  (* formula is not in negation normal form *)
 			(* prop_formula -> int list *)
 			fun forced_vars True              = []
 			  | forced_vars False             = []