prefixed op;
authorwenzelm
Sat Nov 14 13:26:11 1998 +0100 (1998-11-14)
changeset 586430b6a3251813
parent 5863 9935800edf58
child 5865 2303f5a3036d
prefixed op;
src/Pure/General/ROOT.ML
src/Pure/General/seq.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Sat Nov 14 13:25:34 1998 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Sat Nov 14 13:26:11 1998 +0100
     1.3 @@ -12,3 +12,15 @@
     1.4  use "path.ML";
     1.5  use "file.ML";
     1.6  use "history.ML";
     1.7 +
     1.8 +structure PureGeneral =
     1.9 +struct
    1.10 +  structure Symtab = Symtab;
    1.11 +  structure Object = Object;
    1.12 +  structure Seq = Seq;
    1.13 +  structure NameSpace = NameSpace;
    1.14 +  structure Position = Position;
    1.15 +  structure Path = Path;
    1.16 +  structure File = File;
    1.17 +  structure History = History;
    1.18 +end;
     2.1 --- a/src/Pure/General/seq.ML	Sat Nov 14 13:25:34 1998 +0100
     2.2 +++ b/src/Pure/General/seq.ML	Sat Nov 14 13:26:11 1998 +0100
     2.3 @@ -171,14 +171,14 @@
     2.4  fun fail _ = empty;
     2.5  
     2.6  
     2.7 -fun THEN (f, g) x = flat (map g (f x));
     2.8 +fun op THEN (f, g) x = flat (map g (f x));
     2.9  
    2.10 -fun ORELSE (f, g) x =
    2.11 +fun op ORELSE (f, g) x =
    2.12    (case pull (f x) of
    2.13      None => g x
    2.14    | some => make (fn () => some));
    2.15  
    2.16 -fun APPEND (f, g) x =
    2.17 +fun op APPEND (f, g) x =
    2.18    append (f x, make (fn () => pull (g x)));
    2.19  
    2.20