--- 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!*)