src/Tools/code/code_thingol.ML
changeset 27609 b23c9ad0fe7d
parent 27422 73d25d422124
child 27711 5052736b8bcc
     1.1 --- a/src/Tools/code/code_thingol.ML	Tue Jul 15 15:59:49 2008 +0200
     1.2 +++ b/src/Tools/code/code_thingol.ML	Tue Jul 15 16:02:07 2008 +0200
     1.3 @@ -569,18 +569,15 @@
     1.4  (
     1.5    type T = program;
     1.6    val empty = Graph.empty;
     1.7 -  fun merge _ = Graph.merge (K true);
     1.8 -  fun purge _ NONE _ = Graph.empty
     1.9 -    | purge NONE _ _ = Graph.empty
    1.10 -    | purge (SOME thy) (SOME cs) program =
    1.11 -        let
    1.12 -          val cs_exisiting =
    1.13 -            map_filter (CodeName.const_rev thy) (Graph.keys program);
    1.14 -          val dels = (Graph.all_preds program
    1.15 -              o map (CodeName.const thy)
    1.16 -              o filter (member (op =) cs_exisiting)
    1.17 -            ) cs;
    1.18 -        in Graph.del_nodes dels program end;
    1.19 +  fun purge thy cs program =
    1.20 +    let
    1.21 +      val cs_exisiting =
    1.22 +        map_filter (CodeName.const_rev thy) (Graph.keys program);
    1.23 +      val dels = (Graph.all_preds program
    1.24 +          o map (CodeName.const thy)
    1.25 +          o filter (member (op =) cs_exisiting)
    1.26 +        ) cs;
    1.27 +    in Graph.del_nodes dels program end;
    1.28  );
    1.29  
    1.30  val cached_program = Program.get;