# HG changeset patch
# User webertj
# Date 1092493676 -7200
# Node ID da03f05815b0af51b2f562b4accf8448b491a965
# Parent  2550a5578d390217e226610cf2887730f65bcda3
bugfix in read_dimacs_cnf_file

diff -r 2550a5578d39 -r da03f05815b0 src/HOL/Tools/sat_solver.ML
--- 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 =