diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Oct 13 09:21:15 2015 +0200
@@ -884,9 +884,9 @@
     val intro'''' =
       Simplifier.full_simplify
         (put_simpset HOL_basic_ss ctxt
-          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
+          addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.inject}])
       intro'''
-    (* splitting conjunctions introduced by Pair_eq*)
+    (* splitting conjunctions introduced by prod.inject*)
     val intro''''' = split_conjuncts_in_assms ctxt intro''''
   in
     intro'''''