author | webertj |
Sat, 14 Aug 2004 16:27:56 +0200 | |
changeset 15128 | da03f05815b0 |
parent 15127 | 2550a5578d39 |
child 15129 | fbf90acc5bf4 |
--- 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 =