src/Tools/nbe.ML
changeset 27609 b23c9ad0fe7d
parent 27499 150558266831
child 28054 2b84d34c5d02
     1.1 --- a/src/Tools/nbe.ML	Tue Jul 15 15:59:49 2008 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Jul 15 16:02:07 2008 +0200
     1.3 @@ -346,20 +346,15 @@
     1.4  (
     1.5    type T = (Univ option * int) Graph.T * (int * string Inttab.table);
     1.6    val empty = (Graph.empty, (0, Inttab.empty));
     1.7 -  fun merge _ ((gr1, (maxidx1, idx_tab1)), (gr2, (maxidx2, idx_tab2))) =
     1.8 -    (Graph.merge (K true) (gr1, gr2), (IntInf.max (maxidx1, maxidx2),
     1.9 -      Inttab.merge (K true) (idx_tab1, idx_tab2)));
    1.10 -  fun purge _ NONE _ = empty
    1.11 -    | purge NONE _ _ = empty
    1.12 -    | purge (SOME thy) (SOME cs) (gr, (maxidx, idx_tab)) =
    1.13 -        let
    1.14 -          val cs_exisiting =
    1.15 -            map_filter (CodeName.const_rev thy) (Graph.keys gr);
    1.16 -          val dels = (Graph.all_preds gr
    1.17 -              o map (CodeName.const thy)
    1.18 -              o filter (member (op =) cs_exisiting)
    1.19 -            ) cs;
    1.20 -        in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
    1.21 +  fun purge thy cs (gr, (maxidx, idx_tab)) =
    1.22 +    let
    1.23 +      val cs_exisiting =
    1.24 +        map_filter (CodeName.const_rev thy) (Graph.keys gr);
    1.25 +      val dels = (Graph.all_preds gr
    1.26 +          o map (CodeName.const thy)
    1.27 +          o filter (member (op =) cs_exisiting)
    1.28 +        ) cs;
    1.29 +    in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
    1.30  );
    1.31  
    1.32  (* compilation, evaluation and reification *)