src/Tools/Code/code_thingol.ML
changeset 46665 919dfcdf6d8a
parent 46614 165886a4fe64
child 46961 5c6955f487e5
--- a/src/Tools/Code/code_thingol.ML	Fri Feb 24 22:46:44 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sat Feb 25 12:34:56 2012 +0100
@@ -938,7 +938,7 @@
         val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
           Graph.get_node program1 Term.dummy_patternN;
         val deps = Graph.immediate_succs program1 Term.dummy_patternN;
-        val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
+        val program2 = Graph.del_node Term.dummy_patternN program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.restrict (member (op =) deps_all) program2;
       in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;