Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed a "Matches are not exhaustive" warning
authorwebertj
Wed, 24 Nov 2004 19:51:33 +0100
changeset 15329 bd94b0a71dd2
parent 15328 35951e6a7855
child 15330 630981482718
Removed a "Matches are not exhaustive" warning
src/HOL/Tools/sat_solver.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle