SML/NJ compatibility.
authorballarin
Fri, 27 May 2005 17:10:41 +0200
changeset 16105 a44801c499cb
parent 16104 dab13c4685ba
child 16106 c2ea4b171f99
SML/NJ compatibility.
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 *)