author | ballarin |
Fri, 27 May 2005 17:10:41 +0200 | |
changeset 16105 | a44801c499cb |
parent 16104 | dab13c4685ba |
child 16106 | c2ea4b171f99 |
--- 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 *)