diff -r 2cf3d8305b47 -r 5cdba14d20fa src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Tue Aug 31 18:38:36 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Aug 31 19:14:18 2010 +0200
@@ -298,12 +298,13 @@
   let
     val names2 = subtract (op =) names_hidden names1;
     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
-    val names_all = Graph.all_succs program3 names2;
+    val names4 = Graph.all_succs program3 names2;
     val empty_funs = filter_out (member (op =) abortable)
       (Code_Thingol.empty_funs program3);
     val _ = if null empty_funs then () else error ("No code equations for "
       ^ commas (map (Sign.extern_const thy) empty_funs));
-  in (names_all, program3) end;
+    val program4 = Graph.subgraph (member (op =) names4) program3;
+  in (names4, program4) end;
 
 fun invoke_serializer thy abortable serializer literals reserved abs_includes 
     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax