changeset 2042 | 33b4c1624e26 |
parent 1601 | 0ef6ea27ab15 |
child 2672 | 85d7e800d754 |
--- 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;