Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/sat_solver.ML
changeset 15329 bd94b0a71dd2
parent 15313 24aee76539df
child 15332 0dc05858a862 
--- 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