# HG changeset patch
# User ballarin
# Date 1117206641 -7200
# Node ID a44801c499cbc56c888981953fadff3c0eccc58c
# Parent  dab13c4685ba50164dec4d26341702fe0cbd1a10
SML/NJ compatibility.

diff -r dab13c4685ba -r a44801c499cb src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri May 27 17:10:23 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri May 27 17:10:41 2005 +0200
@@ -746,7 +746,7 @@
 
 fun merge_syntax ctxt ids ss = Symtab.merge (op =) ss
   handle Symtab.DUPS xs => err_in_locale ctxt
-    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map #1 ids);
+    ("Conflicting syntax for parameter(s): " ^ commas_quote xs) (map fst ids);
 
 
 (* flatten expressions *)