1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Sep 02 10:29:48 2010 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Sep 02 10:29:49 2010 +0200
     1.3 @@ -105,12 +105,15 @@
     1.4          val (nsps', nodes') = (nsps, nodes)
     1.5            |> fold (declare (K namify_module)) module_fragments
     1.6            |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_names;
     1.7 -        val modify_stmts' = filter (member (op =) stmt_names)
     1.8 -          #> AList.make (snd o Graph.get_node nodes)
     1.9 +        fun zip_fillup xs ys = xs ~~ ys @ replicate (length xs - length ys) NONE;
    1.10 +        fun select_names names = case filter (member (op =) stmt_names) names
    1.11 +         of [] => NONE
    1.12 +          | xs => SOME xs;
    1.13 +        val modify_stmts' = AList.make (snd o Graph.get_node nodes)
    1.14            #> split_list
    1.15            ##> map (fn Stmt stmt => stmt)
    1.16 -          #> (fn (names, stmts) => names ~~ modify_stmts (names ~~ stmts));
    1.17 -        val stmtss' = maps modify_stmts' (Graph.strong_conn nodes);
    1.18 +          #> (fn (names, stmts) => zip_fillup names (modify_stmts (names ~~ stmts)));
    1.19 +        val stmtss' = (maps modify_stmts' o map_filter select_names o Graph.strong_conn) nodes;
    1.20          val nodes'' = Graph.map (fn name => apsnd (fn Module content => Module (make_declarations nsps' content)
    1.21              | _ => case AList.lookup (op =) stmtss' name of SOME (SOME stmt) => Stmt stmt | _ => Dummy)) nodes';
    1.22          val data' = fold memorize_data stmt_names data;