Removed a "Matches are not exhaustive" warning
authorwebertj
Wed Nov 24 19:51:33 2004 +0100 (2004-11-24)
changeset 15329bd94b0a71dd2
parent 15328 35951e6a7855
child 15330 630981482718
Removed a "Matches are not exhaustive" warning
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Nov 24 11:13:00 2004 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Nov 24 19:51:33 2004 +0100
     1.3 @@ -281,6 +281,7 @@
     1.4  				  []      => [xs1]
     1.5  				| (0::[]) => [xs1]
     1.6  				| (0::tl) => xs1 :: clauses tl
     1.7 +				| _       => raise ERROR  (* this cannot happen *)
     1.8  			end
     1.9  		(* int -> PropLogic.prop_formula *)
    1.10  		fun literal_from_int i =