tuned;
authorwenzelm
Thu Nov 09 21:44:28 2006 +0100 (2006-11-09)
changeset 21270b82f4c16355e
parent 21269 c605503bb4ef
child 21271 4f791faf33f4
tuned;
src/Pure/General/seq.ML
     1.1 --- a/src/Pure/General/seq.ML	Thu Nov 09 21:44:27 2006 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Thu Nov 09 21:44:28 2006 +0100
     1.3 @@ -187,12 +187,12 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** sequence functions **)      (*some code copied from Pure/tctical.ML*)
     1.8 +(** sequence functions **)      (*cf. Pure/tctical.ML*)
     1.9  
    1.10  fun succeed x = single x;
    1.11  fun fail _ = empty;
    1.12  
    1.13 -fun op THEN (f, g) x = flat (map g (f x));
    1.14 +fun op THEN (f, g) x = maps g (f x);
    1.15  
    1.16  fun op ORELSE (f, g) x =
    1.17    (case pull (f x) of