diff -r 510d94c71dda -r 85d7e800d754 src/Pure/deriv.ML
--- 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);