src/Tools/code/code_funcgr.ML
changeset 27609 b23c9ad0fe7d
parent 27103 d8549f4d900b
child 28054 2b84d34c5d02
--- a/src/Tools/code/code_funcgr.ML	Tue Jul 15 15:59:49 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Tue Jul 15 16:02:07 2008 +0200
@@ -261,11 +261,9 @@
 (
   type T = T;
   val empty = Graph.empty;
-  fun merge _ _ = Graph.empty;
-  fun purge _ NONE _ = Graph.empty
-    | purge _ (SOME cs) funcgr =
-        Graph.del_nodes ((Graph.all_preds funcgr 
-          o filter (can (Graph.get_node funcgr))) cs) funcgr;
+  fun purge _ cs funcgr =
+    Graph.del_nodes ((Graph.all_preds funcgr 
+      o filter (can (Graph.get_node funcgr))) cs) funcgr;
 );
 
 fun make thy =