diff -r bf18c8174571 -r ca77d8c34ce2 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -89,6 +89,13 @@
     []
   else [intro]
 
+
+fun print_intross thy msg intross =
+  tracing (msg ^ 
+    (space_implode "; " (map 
+      (fn intros => commas (map (Display.string_of_thm_global thy) intros)) intross)))
+
+  
 fun preprocess_strong_conn_constnames gr constnames thy =
   let
     val get_specs = map (fn k => (k, Graph.get_node gr k))
@@ -103,8 +110,7 @@
     val _ = priority "Compiling predicates to flat introrules..."
     val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
       (get_specs prednames) thy')
-    val _ = tracing ("Flattened introduction rules: " ^
-      commas (map (Display.string_of_thm_global thy'') (flat intross1)))
+    val _ = print_intross thy'' "Flattened introduction rules: " intross1
     val _ = priority "Replacing functions in introrules..."
       (*  val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross  *)
     val intross2 =
@@ -113,11 +119,12 @@
           SOME intross => intross
         | NONE => let val _ = warning "Function replacement failed!" in intross1 end
       else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
-    val _ = tracing ("Introduction rules with replaced functions: " ^
-      commas (map (Display.string_of_thm_global thy'') (flat intross2)))
-    val intross3 = burrow (maps remove_pointless_clauses) intross2
+    val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2
+    val intross3 = map (maps remove_pointless_clauses) intross2
+    val _ = print_intross thy'' "After removing pointless clauses: " intross3
     val intross4 = burrow (map (AxClass.overload thy'')) intross3
     val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4
+    val _ = print_intross thy'' "introduction rules before registering: " intross5
     val _ = priority "Registering intro rules..."
     val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy''
   in