# HG changeset patch
# User wenzelm
# Date 1169240910 -3600
# Node ID 1950ae4fe5e03f0f90e421ccb86346f449391076
# Parent  8424ef945cb50bf56c9d2632fa72ed26a3f1e91b
tuned Scan.extend_lexicon;

diff -r 8424ef945cb5 -r 1950ae4fe5e0 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)),