diff -r 62156e694f3d -r 68c5104d2204 src/HOL/ex/Coercion_Examples.thy
--- a/src/HOL/ex/Coercion_Examples.thy	Thu Mar 06 13:36:15 2014 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Thu Mar 06 13:36:48 2014 +0100
@@ -52,10 +52,10 @@
 
 declare [[coercion_map "\<lambda> f g h . g o h o f"]]
 
-primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
- "map_pair f g (x,y) = (f x, g y)"
+primrec map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
+ "map_prod f g (x,y) = (f x, g y)"
 
-declare [[coercion_map map_pair]]
+declare [[coercion_map map_prod]]
 
 (* Examples taken from the haskell draft implementation *)