--- a/src/HOL/Tools/function_package/fundef_lib.ML Sun Jun 11 19:36:10 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Sun Jun 11 21:59:17 2006 +0200
@@ -54,7 +54,7 @@
fun map3 _ [] [] [] = []
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
- | map3 _ _ _ _ = raise UnequalLengths;
+ | map3 _ _ _ _ = raise Library.UnequalLengths;
@@ -64,4 +64,4 @@
fun the_single [x] = x
- | the_single _ = sys_error "the_single"
\ No newline at end of file
+ | the_single _ = sys_error "the_single"