# HG changeset patch
# User wenzelm
# Date 911046371 -3600
# Node ID 30b6a32518130fc30d6a52284c7235e73bf8c10e
# Parent  9935800edf587711c22248a8749f168c7f9c70fc
prefixed op;

diff -r 9935800edf58 -r 30b6a3251813 src/Pure/General/ROOT.ML
--- 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;
diff -r 9935800edf58 -r 30b6a3251813 src/Pure/General/seq.ML
--- 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)));