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.
strict forall2
authorhaftmann
Fri, 26 Nov 2010 23:13:58 +0100
changeset 40731 4e60c7348096
parent 40730 2aa0390a2da7
child 40732 4375cc6f1a7e
strict forall2
src/Pure/library.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/library.ML	Fri Nov 26 23:13:58 2010 +0100
+++ b/src/Pure/library.ML	Fri Nov 26 23:13:58 2010 +0100
@@ -546,7 +546,7 @@
 
 fun forall2 P [] [] = true
   | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
-  | forall2 P _ _ = false;
+  | forall2 P _ _ = raise UnequalLengths;
 
 fun map_split f [] = ([], [])
   | map_split f (x :: xs) =
isabelle