# HG changeset patch
# User haftmann
# Date 1151395779 -7200
# Node ID fd74bf4e603ed707a01aad0af75d57ff17b00fff
# Parent  0505dce27b0b4b240bb64fc85d10ce9a14b4acab
replaced subgraph by project

diff -r 0505dce27b0b -r fd74bf4e603e src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Jun 24 22:54:37 2006 +0200
+++ b/src/Pure/General/graph.ML	Tue Jun 27 10:09:39 2006 +0200
@@ -29,7 +29,7 @@
   val all_preds: 'a T -> key list -> key list
   val all_succs: 'a T -> key list -> key list
   val strong_conn: 'a T -> key list list
-  val subgraph: key list -> 'a T -> 'a T
+  val project: (key -> bool) -> 'a T -> 'a T
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
@@ -141,11 +141,10 @@
   (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
 
 (*subgraph induced by node subset*)
-fun subgraph keys G =
+fun project proj G =
   let
-    val select = member eq_key keys;
     fun subg (k, (i, (preds, succs))) =
-      K (select k) ? Table.update (k, (i, (filter select preds, filter select succs)));
+      K (proj k) ? Table.update (k, (i, (filter proj preds, filter proj succs)));
   in Graph (fold_graph subg G Table.empty) end;