1.1 --- a/src/Tools/code/code_name.ML	Tue Jul 15 15:59:49 2008 +0200
     1.2 +++ b/src/Tools/code/code_name.ML	Tue Jul 15 16:02:07 2008 +0200
     1.3 @@ -303,12 +303,8 @@
     1.4  (
     1.5    type T = const Symtab.table * string Symtab.table;
     1.6    val empty = (Symtab.empty, Symtab.empty);
     1.7 -  fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
     1.8 -    (Symtab.merge (op =) (const1, const2),
     1.9 -      Symtab.merge (op =) (constrev1, constrev2));
    1.10 -  fun purge _ NONE _ = empty
    1.11 -    | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
    1.12 -        fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
    1.13 +  fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const,
    1.14 +    fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
    1.15  );
    1.16  
    1.17  val setup = CodeName.init;