src/HOL/ex/predicate_compile.ML

   val code_pred_cmd: string -> Proof.context -> Proof.state
 (*  val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *)
   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;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
 struct

     |> filter (is_inductive_predicate thy)
   in
     (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)
     val scc = strong_conn_of (PredData.get thy') [name]
     val thy'' = fold_rev add_equations_of scc thy'

 fun generic_code_pred prep_const raw_const lthy =
   let
     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)
     (*
     fun mk_elim pred =
       let