src/Pure/deriv.ML
changeset 2042 33b4c1624e26
parent 1601 0ef6ea27ab15
child 2672 85d7e800d754
     1.1 --- a/src/Pure/deriv.ML	Thu Sep 26 17:30:52 1996 +0200
     1.2 +++ b/src/Pure/deriv.ML	Thu Sep 26 17:34:36 1996 +0200
     1.3 @@ -142,7 +142,8 @@
     1.4  (*Currently declared at end, to avoid conflicting with library's drop
     1.5    Can put it after "size" once we switch to List.drop*)
     1.6  fun drop (der,0) = der
     1.7 -  | drop (Join (_, der::_), n) = drop (der, n-1);
     1.8 +  | drop (Join (_, der::_), n) = drop (der, n-1)
     1.9 +  | drop (der,_) = der;
    1.10  
    1.11  end;
    1.12