# HG changeset patch
# User paulson
# Date 843752076 -7200
# Node ID 33b4c1624e2606670c0141219081b96549881095
# Parent  a3262b93c1d2eec6b9e7bbd76c5e5e5ed2694cd9
Added catch-all clause to drop, preventing exception Match

diff -r a3262b93c1d2 -r 33b4c1624e26 src/Pure/deriv.ML
--- a/src/Pure/deriv.ML	Thu Sep 26 17:30:52 1996 +0200
+++ b/src/Pure/deriv.ML	Thu Sep 26 17:34:36 1996 +0200
@@ -142,7 +142,8 @@
 (*Currently declared at end, to avoid conflicting with library's drop
   Can put it after "size" once we switch to List.drop*)
 fun drop (der,0) = der
-  | drop (Join (_, der::_), n) = drop (der, n-1);
+  | drop (Join (_, der::_), n) = drop (der, n-1)
+  | drop (der,_) = der;
 
 end;