diff -r 2a4cec6bcae2 -r 43fecedff8cf src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Tue Apr 20 13:44:28 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Wed Apr 21 12:10:52 2010 +0200
@@ -107,7 +107,9 @@
     val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
       [list_comb (pred, pats), list_comb (specialised_const, result_pats)]
     val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy'
-    val ([spec], thy''') = find_specialisations black_list [(constname, exported_intros)] thy''
+    val optimised_intros =
+      map_filter (Predicate_Compile_Aux.peephole_optimisation thy'') exported_intros
+    val ([spec], thy''') = find_specialisations black_list [(constname, optimised_intros)] thy''
     val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
   in
     thy''''