# HG changeset patch
# User wenzelm
# Date 771152437 -7200
# Node ID 6bb9eb9cb02f8527f1ea6f4f9cd1edabfec27eca
# Parent  12f9f36e4484d0ff39daf9a1cd76328d1c23becb
new datatype 'mixfix' now pervasive (old one still accesible via OldMixfix);

diff -r 12f9f36e4484 -r 6bb9eb9cb02f src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Thu Jun 09 11:00:01 1994 +0200
+++ b/src/Pure/Syntax/ROOT.ML	Thu Jun 09 11:00:37 1994 +0200
@@ -10,7 +10,6 @@
 use "ast.ML";
 use "syn_ext.ML";
 use "parser.ML";
-(*use "earley0A.ML";*)      (* FIXME remove *)
 use "type_ext.ML";
 use "sextension.ML";
 use "mixfix.ML";
@@ -24,8 +23,6 @@
 structure SynExt = SynExtFun(structure Lexicon = Lexicon and Ast = Ast);
 structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon
   and SynExt = SynExt);
-(*structure Earley = EarleyFun(structure Symtab = Symtab and Lexicon = Lexicon
-  and SynExt = SynExt);*)     (* FIXME remove *)
 structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt);
 structure SExtension = SExtensionFun(structure TypeExt = TypeExt and Parser = Parser);
 structure Mixfix = MixfixFun(structure Lexicon = Lexicon and SynExt = SynExt and
@@ -36,5 +33,6 @@
   and SExtension = SExtension and Mixfix = Mixfix and Printer = Printer);
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
 
-structure OldMixfix: SEXTENSION0 = SExtension;   (* FIXME *)
-
+(* FIXME tmp hacks *)
+structure BasicSyntax = struct open BasicSyntax Mixfix end;
+structure OldMixfix: SEXTENSION0 = SExtension;