changeset 2672 | 85d7e800d754 |
parent 2042 | 33b4c1624e26 |
child 6085 | 3d8dcb09dbfb |
--- a/src/Pure/deriv.ML Fri Feb 21 15:30:41 1997 +0100 +++ b/src/Pure/deriv.ML Fri Feb 21 15:31:47 1997 +0100 @@ -38,7 +38,7 @@ Join (Bicompose arg, linear rder) :: rev_deriv sder | rev_deriv (Join (_, [der])) = rev_deriv der | rev_deriv (Join (rl, der::ders)) = (*catch-all case; doubtful?*) - Join(rl, flat (map linear ders)) :: rev_deriv der + Join(rl, List.concat (map linear ders)) :: rev_deriv der and linear der = rev (rev_deriv der);