diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/SMT_Examples/SMT_Tests.thy
--- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -506,7 +506,7 @@
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
-  using fst_conv snd_conv pair_collapse
+  using fst_conv snd_conv prod.collapse
   by smt+
 
 lemma
@@ -525,7 +525,7 @@
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
-  using fst_conv snd_conv pair_collapse list.sel(1,3) list.simps
+  using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps
   by smt+
 
 
@@ -627,7 +627,7 @@
   "p1 = (x, y) \<and> p2 = (y, x) \<longrightarrow> fst p1 = snd p2"
   "(fst (x, y) = snd (x, y)) = (x = y)"
   "(fst p = snd p) = (p = (snd p, fst p))"
-  using fst_conv snd_conv pair_collapse
+  using fst_conv snd_conv prod.collapse
   using [[smt_oracle, z3_extensions]]
   by smt+
 
@@ -648,7 +648,7 @@
 lemma
   "fst (hd [(a, b)]) = a"
   "snd (hd [(a, b)]) = b"
-  using fst_conv snd_conv pair_collapse list.sel(1,3)
+  using fst_conv snd_conv prod.collapse list.sel(1,3)
   using [[smt_oracle, z3_extensions]]
   by smt+