tuned Scan.extend_lexicon;
authorwenzelm
Fri, 19 Jan 2007 22:08:30 +0100
changeset 22121 1950ae4fe5e0
parent 22120 8424ef945cb5
child 22122 58f846cc5c3d
tuned Scan.extend_lexicon;
src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Jan 19 22:08:29 2007 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Jan 19 22:08:30 2007 +0100
@@ -223,7 +223,7 @@
   in
     Syntax
     ({input = if_inout xprods @ input,
-      lexicon = Scan.extend_lexicon lexicon (if_inout (SynExt.delims_of xprods)),
+      lexicon = Scan.extend_lexicon (if_inout (SynExt.delims_of xprods)) lexicon,
       gram = Parser.extend_gram gram (if_inout xprods),
       consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),