--- a/src/HOL/ex/predicate_compile.ML Tue Jun 09 13:56:28 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Tue Jun 09 14:20:37 2009 +0200
@@ -24,7 +24,6 @@
val do_proofs: bool ref
val analyze_compr: theory -> term -> term
val eval_ref: (unit -> term Predicate.pred) option ref
- (* val extend : (key -> 'a * key list) -> key list -> 'a Graph.T -> 'a Graph.T *)
val add_equations : string -> theory -> theory
end;
@@ -1383,25 +1382,9 @@
(data, keys)
end;
-fun extend explore keys gr =
- let
- fun contains_node gr key = member (op =) (Graph.keys gr) key
- fun extend' key gr =
- let
- val (node, preds) = explore key
- in
- gr |> (not (contains_node gr key)) ?
- (Graph.new_node (key, node)
- #> fold extend' preds
- #> fold (Graph.add_edge o (pair key)) preds)
- end
- in fold extend' keys gr end
-
-fun mk_graph explore keys = extend explore keys Graph.empty
-
fun add_equations name thy =
let
- val thy' = PredData.map (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)
@@ -1427,7 +1410,7 @@
val thy = (ProofContext.theory_of lthy)
val const = prep_const thy raw_const
val lthy' = lthy
- val thy' = PredData.map (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)
(*