# HG changeset patch
# User haftmann
# Date 1290809638 -3600
# Node ID 4e60c7348096381914a64b0c75a4465b2c4bf32c
# Parent  2aa0390a2da702468266edbfc310d2bf8fba0799
strict forall2

diff -r 2aa0390a2da7 -r 4e60c7348096 src/Pure/library.ML
--- 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) =