changeset 21270 | b82f4c16355e |
parent 20332 | 27e4f43a0c3e |
child 21395 | f34ac19659ae |
--- 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