1.1 --- a/src/Pure/Isar/method.ML	Sun Jul 08 19:51:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sun Jul 08 19:51:58 2007 +0200
     1.3 @@ -389,8 +389,8 @@
     1.4    val empty = NameSpace.empty_table;
     1.5    val copy = I;
     1.6    val extend = I;
     1.7 -  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUPS dups =>
     1.8 -    error ("Attempt to merge different versions of method(s) " ^ commas_quote dups);
     1.9 +  fun merge _ tables : T = NameSpace.merge_tables (eq_snd (op =)) tables handle Symtab.DUP dup =>
    1.10 +    error ("Attempt to merge different versions of method " ^ quote dup);
    1.11  );
    1.12  
    1.13  fun print_methods thy =
    1.14 @@ -430,8 +430,7 @@
    1.15        (name, ((f, comment), stamp ())));
    1.16  
    1.17      fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
    1.18 -      handle Symtab.DUPS dups =>
    1.19 -        error ("Duplicate declaration of method(s) " ^ commas_quote dups);
    1.20 +      handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
    1.21    in MethodsData.map add thy end;
    1.22  
    1.23  val add_method = add_methods o Library.single;