src/Pure/Syntax/ROOT.ML

--- a/src/Pure/Syntax/ROOT.ML	Thu May 19 16:30:56 1994 +0200
+++ b/src/Pure/Syntax/ROOT.ML	Thu May 19 16:42:04 1994 +0200
@@ -10,9 +10,10 @@
 use "ast.ML";
 use "syn_ext.ML";
 use "parser.ML";
-(*use "earley0A.ML";*)
+(*use "earley0A.ML";*)      (* FIXME remove *)
 use "type_ext.ML";
 use "sextension.ML";
+use "mixfix.ML";
 use "printer.ML";
 use "syntax.ML";
 
@@ -24,11 +25,16 @@
 structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon
   and SynExt = SynExt);
 (*structure Earley = EarleyFun(structure Symtab = Symtab and Lexicon = Lexicon
-  and SynExt = SynExt);*)
+  and SynExt = SynExt);*)     (* FIXME remove *)
 structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt);
-structure SExtension = SExtensionFun(Parser);
+structure SExtension = SExtensionFun(structure TypeExt = TypeExt and Parser = Parser);
+structure Mixfix = MixfixFun(structure Lexicon = Lexicon and SynExt = SynExt and
+  SExtension = SExtension);
 structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt
   and SExtension = SExtension);
 structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
-  and SExtension = SExtension and Printer = Printer);
+  and SExtension = SExtension and Mixfix = Mixfix and Printer = Printer);
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
+
+structure OldMixfix: SEXTENSION0 = SExtension;   (* FIXME *)
+