--- a/src/Pure/Syntax/syntax.ML Mon Feb 15 17:17:51 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Feb 15 18:03:42 2010 +0100
@@ -450,9 +450,9 @@
fun guess_infix (Syntax ({gram, ...}, _)) c =
(case Parser.guess_infix_lr gram c of
SOME (s, l, r, j) => SOME
- (if l then Mixfix.InfixlName (s, j)
- else if r then Mixfix.InfixrName (s, j)
- else Mixfix.InfixName (s, j))
+ (if l then Mixfix.Infixl (s, j)
+ else if r then Mixfix.Infixr (s, j)
+ else Mixfix.Infix (s, j))
| NONE => NONE);
@@ -914,8 +914,8 @@
end;
-structure BasicSyntax: BASIC_SYNTAX = Syntax;
-open BasicSyntax;
+structure Basic_Syntax: BASIC_SYNTAX = Syntax;
+open Basic_Syntax;
forget_structure "Ast";
forget_structure "SynExt";