diff -r 8fd5662ccd97 -r b23c9ad0fe7d src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/nbe.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -346,20 +346,15 @@
 (
   type T = (Univ option * int) Graph.T * (int * string Inttab.table);
   val empty = (Graph.empty, (0, Inttab.empty));
-  fun merge _ ((gr1, (maxidx1, idx_tab1)), (gr2, (maxidx2, idx_tab2))) =
-    (Graph.merge (K true) (gr1, gr2), (IntInf.max (maxidx1, maxidx2),
-      Inttab.merge (K true) (idx_tab1, idx_tab2)));
-  fun purge _ NONE _ = empty
-    | purge NONE _ _ = empty
-    | purge (SOME thy) (SOME cs) (gr, (maxidx, idx_tab)) =
-        let
-          val cs_exisiting =
-            map_filter (CodeName.const_rev thy) (Graph.keys gr);
-          val dels = (Graph.all_preds gr
-              o map (CodeName.const thy)
-              o filter (member (op =) cs_exisiting)
-            ) cs;
-        in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
+  fun purge thy cs (gr, (maxidx, idx_tab)) =
+    let
+      val cs_exisiting =
+        map_filter (CodeName.const_rev thy) (Graph.keys gr);
+      val dels = (Graph.all_preds gr
+          o map (CodeName.const thy)
+          o filter (member (op =) cs_exisiting)
+        ) cs;
+    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
 );
 
 (* compilation, evaluation and reification *)