Added catch-all clause to drop, preventing exception Match
authorpaulson
Thu Sep 26 17:34:36 1996 +0200 (1996-09-26)
changeset 204233b4c1624e26
parent 2041 a3262b93c1d2
child 2043 8de7a0ab463b
Added catch-all clause to drop, preventing exception Match
src/Pure/deriv.ML
     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