--- a/src/Pure/General/ROOT.ML Sat Nov 14 13:25:34 1998 +0100
+++ b/src/Pure/General/ROOT.ML Sat Nov 14 13:26:11 1998 +0100
@@ -12,3 +12,15 @@
use "path.ML";
use "file.ML";
use "history.ML";
+
+structure PureGeneral =
+struct
+ structure Symtab = Symtab;
+ structure Object = Object;
+ structure Seq = Seq;
+ structure NameSpace = NameSpace;
+ structure Position = Position;
+ structure Path = Path;
+ structure File = File;
+ structure History = History;
+end;
--- a/src/Pure/General/seq.ML Sat Nov 14 13:25:34 1998 +0100
+++ b/src/Pure/General/seq.ML Sat Nov 14 13:26:11 1998 +0100
@@ -171,14 +171,14 @@
fun fail _ = empty;
-fun THEN (f, g) x = flat (map g (f x));
+fun op THEN (f, g) x = flat (map g (f x));
-fun ORELSE (f, g) x =
+fun op ORELSE (f, g) x =
(case pull (f x) of
None => g x
| some => make (fn () => some));
-fun APPEND (f, g) x =
+fun op APPEND (f, g) x =
append (f x, make (fn () => pull (g x)));