merged

--- a/src/HOL/ex/predicate_compile.ML	Tue Jun 09 23:02:01 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Wed Jun 10 10:09:30 2009 +0200
@@ -1384,7 +1384,7 @@
 
 fun add_equations name thy =
   let
-    val thy' = PredData.map (Graph.extend (dependencies_of thy) [name]) thy;
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy;
     (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *)
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -1413,7 +1413,7 @@
     val thy = (ProofContext.theory_of lthy)
     val const = prep_const thy raw_const
     val lthy' = lthy
-    val thy' = PredData.map (Graph.extend (dependencies_of thy) [const]) thy
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) const) thy
     val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
     val _ = Output.tracing ("preds: " ^ commas preds)
     (*

--- a/src/Pure/General/graph.ML	Tue Jun 09 23:02:01 2009 +0200
+++ b/src/Pure/General/graph.ML	Wed Jun 10 10:09:30 2009 +0200
@@ -48,8 +48,7 @@
   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
+  val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
@@ -277,24 +276,21 @@
   |> 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
+    fun ext x G =
+      if can (get_entry G) x then G
+      else
+        let val (info, ys) = explore x in
+          G
+          |> new_node (x, info)
+          |> fold ext ys
+          |> fold (fn y => add_edge (x, y)) ys
+        end
+  in ext end;
 
 
 (*final declarations of this structure!*)