src/Tools/Code/code_target.ML
changeset 38936 5cdba14d20fa
parent 38933 bd77e092f67c
child 39034 ebeb48fd653b
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 18:38:36 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 19:14:18 2010 +0200
     1.3 @@ -298,12 +298,13 @@
     1.4    let
     1.5      val names2 = subtract (op =) names_hidden names1;
     1.6      val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
     1.7 -    val names_all = Graph.all_succs program3 names2;
     1.8 +    val names4 = Graph.all_succs program3 names2;
     1.9      val empty_funs = filter_out (member (op =) abortable)
    1.10        (Code_Thingol.empty_funs program3);
    1.11      val _ = if null empty_funs then () else error ("No code equations for "
    1.12        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.13 -  in (names_all, program3) end;
    1.14 +    val program4 = Graph.subgraph (member (op =) names4) program3;
    1.15 +  in (names4, program4) end;
    1.16  
    1.17  fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    1.18      module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax