bugfix in read_dimacs_cnf_file

--- a/src/HOL/Tools/sat_solver.ML	Thu Aug 12 10:01:09 2004 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sat Aug 14 16:27:56 2004 +0200
@@ -277,7 +277,10 @@
 			let
 				val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
 			in
-				xs1 :: clauses (tl xs2)
+				case xs2 of
+				  []      => [xs1]
+				| (0::[]) => [xs1]
+				| (0::tl) => xs1 :: clauses tl
 			end
 		(* int -> PropLogic.prop_formula *)
 		fun literal_from_int i =