# HG changeset patch
# User bulwahn
# Date 1280417271 -7200
# Node ID 7b8c295af291b1a08bfbf0a41cbb9e73649d9332
# Parent  aaeb6f0b1b1d923e77d078088b02dea706809970
exporting retrieval function for graph of introduction rules in the predicate compiler core

diff -r aaeb6f0b1b1d -r 7b8c295af291 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jul 29 15:07:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jul 29 17:27:51 2010 +0200
@@ -27,6 +27,7 @@
   val all_modes_of : compilation -> Proof.context -> (string * mode list) list
   val all_random_modes_of : Proof.context -> (string * mode list) list
   val intros_of : Proof.context -> string -> thm list
+  val intros_graph_of : Proof.context -> thm list Graph.T
   val add_intro : thm -> theory -> theory
   val set_elim : thm -> theory -> theory
   val register_alternative_function : string -> mode -> string -> theory -> theory
@@ -295,6 +296,9 @@
 
 val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
 
+val intros_graph_of =
+  Graph.map_nodes (#intros o rep_pred_data) o PredData.get o ProofContext.theory_of
+
 (* diagnostic display functions *)
 
 fun print_modes options modes =