tuned;

--- a/src/Pure/General/seq.ML	Thu Nov 09 21:44:27 2006 +0100
+++ b/src/Pure/General/seq.ML	Thu Nov 09 21:44:28 2006 +0100
@@ -187,12 +187,12 @@
 
 
 
-(** sequence functions **)      (*some code copied from Pure/tctical.ML*)
+(** sequence functions **)      (*cf. Pure/tctical.ML*)
 
 fun succeed x = single x;
 fun fail _ = empty;
 
-fun op THEN (f, g) x = flat (map g (f x));
+fun op THEN (f, g) x = maps g (f x);
 
 fun op ORELSE (f, g) x =
   (case pull (f x) of