diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/UNITY/Extend.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -127,7 +127,7 @@
      assumes surj_h: "surj h"
          and prem:   "!! x y. g (h(x,y)) = x"
      shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
+by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
 
 
 subsection{*Trivial properties of f, g, h*}