--- 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 =