diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Oct 13 09:21:15 2015 +0200
@@ -698,7 +698,7 @@
               (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
                 rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
                 dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
-                dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
+                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
                 REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
                   @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
                 hyp_subst_tac ctxt,
@@ -712,7 +712,7 @@
           REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
           EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
             dtac ctxt set_rev_mp, assume_tac ctxt,
-            dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
+            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
             REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
               @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
             hyp_subst_tac ctxt,