# HG changeset patch
# User bulwahn
# Date 1269876640 -7200
# Node ID d606ca1674a7ce07b8c3ec9780e4d32040614687
# Parent  c0fa8499e3661370e3ed3621cd23d535c10f7019
adding a hook for experiments in the predicate compilation process

diff -r c0fa8499e366 -r d606ca1674a7 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:40 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:40 2010 +0200
@@ -9,6 +9,7 @@
   val setup : theory -> theory
   val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
   val present_graph : bool Unsynchronized.ref
+  val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
 end;
 
 structure Predicate_Compile (*: PREDICATE_COMPILE*) =
@@ -16,6 +17,9 @@
 
 val present_graph = Unsynchronized.ref false
 
+val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
+  
+
 open Predicate_Compile_Aux;
 
 (* Some last processing *)
@@ -114,6 +118,7 @@
         map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross5
       val intross7 = map_specs (map (expand_tuples thy''')) intross6
       val intross8 = map_specs (map (eta_contract_ho_arguments thy''')) intross7
+      val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy''')) intross8; ())
       val _ = print_intross options thy''' "introduction rules before registering: " intross8
       val _ = print_step options "Registering introduction rules..."
       val thy'''' = fold Predicate_Compile_Core.register_intros intross8 thy'''