src/Pure/Syntax/syntax.ML
changeset 35130 0991c84e8dcf
parent 35111 18cd034922ba
child 35263 9927471cca35
--- 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";