bugfix in read_dimacs_cnf_file
authorwebertj
Sat Aug 14 16:27:56 2004 +0200 (2004-08-14)
changeset 15128da03f05815b0
parent 15127 2550a5578d39
child 15129 fbf90acc5bf4
bugfix in read_dimacs_cnf_file
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Aug 12 10:01:09 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Aug 14 16:27:56 2004 +0200
     1.3 @@ -277,7 +277,10 @@
     1.4  			let
     1.5  				val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
     1.6  			in
     1.7 -				xs1 :: clauses (tl xs2)
     1.8 +				case xs2 of
     1.9 +				  []      => [xs1]
    1.10 +				| (0::[]) => [xs1]
    1.11 +				| (0::tl) => xs1 :: clauses tl
    1.12  			end
    1.13  		(* int -> PropLogic.prop_formula *)
    1.14  		fun literal_from_int i =