1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jul 29 15:07:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jul 29 17:27:51 2010 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val all_modes_of : compilation -> Proof.context -> (string * mode list) list
     1.5    val all_random_modes_of : Proof.context -> (string * mode list) list
     1.6    val intros_of : Proof.context -> string -> thm list
     1.7 +  val intros_graph_of : Proof.context -> thm list Graph.T
     1.8    val add_intro : thm -> theory -> theory
     1.9    val set_elim : thm -> theory -> theory
    1.10    val register_alternative_function : string -> mode -> string -> theory -> theory
    1.11 @@ -295,6 +296,9 @@
    1.12  
    1.13  val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
    1.14  
    1.15 +val intros_graph_of =
    1.16 +  Graph.map_nodes (#intros o rep_pred_data) o PredData.get o ProofContext.theory_of
    1.17 +
    1.18  (* diagnostic display functions *)
    1.19  
    1.20  fun print_modes options modes =