src/Tools/code/code_name.ML
changeset 27609 b23c9ad0fe7d
parent 27549 0525f5785155
child 28016 b46f48256dab
--- a/src/Tools/code/code_name.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/code/code_name.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -303,12 +303,8 @@
 (
   type T = const Symtab.table * string Symtab.table;
   val empty = (Symtab.empty, Symtab.empty);
-  fun merge _ ((const1, constrev1), (const2, constrev2)) : T =
-    (Symtab.merge (op =) (const1, const2),
-      Symtab.merge (op =) (constrev1, constrev2));
-  fun purge _ NONE _ = empty
-    | purge _ (SOME cs) (const, constrev) = (fold Symtab.delete_safe cs const,
-        fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
+  fun purge _ cs (const, constrev) = (fold Symtab.delete_safe cs const,
+    fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
 );
 
 val setup = CodeName.init;