--- 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 *)