src/Pure/General/seq.ML
changeset 5864 30b6a3251813
parent 5558 64a8495201d1
child 6118 caa439435666
     1.1 --- a/src/Pure/General/seq.ML	Sat Nov 14 13:25:34 1998 +0100
     1.2 +++ b/src/Pure/General/seq.ML	Sat Nov 14 13:26:11 1998 +0100
     1.3 @@ -171,14 +171,14 @@
     1.4  fun fail _ = empty;
     1.5  
     1.6  
     1.7 -fun THEN (f, g) x = flat (map g (f x));
     1.8 +fun op THEN (f, g) x = flat (map g (f x));
     1.9  
    1.10 -fun ORELSE (f, g) x =
    1.11 +fun op ORELSE (f, g) x =
    1.12    (case pull (f x) of
    1.13      None => g x
    1.14    | some => make (fn () => some));
    1.15  
    1.16 -fun APPEND (f, g) x =
    1.17 +fun op APPEND (f, g) x =
    1.18    append (f x, make (fn () => pull (g x)));
    1.19  
    1.20