| changeset 16105 | a44801c499cb |
| parent 16103 | 323838df22fd |
| child 16144 | e339119f4261 |
--- 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 *)