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;