src/Pure/deriv.ML
changeset 2042 33b4c1624e26
parent 1601 0ef6ea27ab15
child 2672 85d7e800d754
equal deleted inserted replaced
2041:a3262b93c1d2 2042:33b4c1624e26
   140 fun tree der = tree_aux (der,[]);
   140 fun tree der = tree_aux (der,[]);
   141 
   141 
   142 (*Currently declared at end, to avoid conflicting with library's drop
   142 (*Currently declared at end, to avoid conflicting with library's drop
   143   Can put it after "size" once we switch to List.drop*)
   143   Can put it after "size" once we switch to List.drop*)
   144 fun drop (der,0) = der
   144 fun drop (der,0) = der
   145   | drop (Join (_, der::_), n) = drop (der, n-1);
   145   | drop (Join (_, der::_), n) = drop (der, n-1)
       
   146   | drop (der,_) = der;
   146 
   147 
   147 end;
   148 end;
   148 
   149 
   149 
   150 
   150 (*We do NOT open this structure*)
   151 (*We do NOT open this structure*)