# HG changeset patch
# User webertj
# Date 1101322293 -3600
# Node ID bd94b0a71dd201781e4ac5f9bd44d01bb1331010
# Parent  35951e6a785533fca26cdf79a50b39a8564f792a
Removed a "Matches are not exhaustive" warning

diff -r 35951e6a7855 -r bd94b0a71dd2 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Nov 24 11:13:00 2004 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Wed Nov 24 19:51:33 2004 +0100
@@ -281,6 +281,7 @@
 				  []      => [xs1]
 				| (0::[]) => [xs1]
 				| (0::tl) => xs1 :: clauses tl
+				| _       => raise ERROR  (* this cannot happen *)
 			end
 		(* int -> PropLogic.prop_formula *)
 		fun literal_from_int i =