src/Tools/code/code_funcgr.ML

 
 structure Funcgr = CodeDataFun
 (
   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 =
   Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);