src/Pure/General/graph.ML

   val is_empty: 'a T -> bool
   val keys: 'a T -> key list
   val dest: 'a T -> (key * key list) list
   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
   val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
-  val subgraph: (key -> bool) -> 'a T -> 'a T
   val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
   val map: (key -> 'a -> 'b) -> 'a T -> 'b T

   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
+  val restrict: (key -> bool) -> 'a T -> 'a T
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a T * 'a T -> 'a T                                               (*exception DUP*)
   val irreducible_paths: 'a T -> key * key -> key list list
   val all_paths: 'a T -> key * key -> key list list

 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
 
 fun get_first f (Graph tab) = Table.get_first f tab;
 fun fold_graph f (Graph tab) = Table.fold f tab;
 
-fun subgraph P G =
-  let
-    fun subg (k, (i, (preds, succs))) =
-      if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
-      else I;
-  in Graph (fold_graph subg G Table.empty) end;
-
 fun get_entry (Graph tab) x =
   (case Table.lookup_key tab x of
     SOME entry => entry
   | NONE => raise UNDEF x);
 

     Graph (tab
       |> Table.delete x
       |> Keys.fold (del_adjacent apsnd) preds
       |> Keys.fold (del_adjacent apfst) succs)
   end;
+
+fun restrict pred G =
+  fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
 
 
 (* edges *)
 
 fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;