| changeset 40731 | 4e60c7348096 |
| parent 40627 | becf5d5187cc |
| child 40733 | a71f786d20da |
--- 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) =