src/Pure/General/graph.ML

   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
   val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
+  val extend: (key -> 'a * key list) -> key list -> 'a T -> 'a T
+  val make: (key -> 'a * key list) -> key list -> 'a T
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
 struct
 

 fun merge_trans_acyclic eq (G1, G2) =
   merge_acyclic eq (G1, G2)
   |> fold add_edge_trans_acyclic (diff_edges G1 G2)
   |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
+  
+(* constructing graphs *)
+
+fun extend explore =
+  let
+    fun contains_node gr key = member eq_key (keys gr) key
+    fun extend' key gr =
+      let
+        val (node, preds) = explore key
+      in
+        gr |> (not (contains_node gr key)) ?
+          (new_node (key, node)
+          #> fold extend' preds
+          #> fold (add_edge o (pair key)) preds)
+      end
+  in fold extend' end
+
+fun make explore keys = extend explore keys empty
+
 
 (*final declarations of this structure!*)
 val fold = fold_graph;
 
 end;