diff -r 9118eb4eb8dc -r ba961a606c67 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Dec 03 15:25:14 2010 +0100
+++ b/src/HOL/RealDef.thy	Mon Dec 06 19:54:48 2010 +0100
@@ -1114,6 +1114,10 @@
 declare [[coercion "real::int\<Rightarrow>real"]]
 declare [[coercion "int"]]
 
+declare [[coercion_map map]]
+declare [[coercion_map "% f g h . g o h o f"]]
+declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
+
 lemma real_eq_of_nat: "real = of_nat"
   unfolding real_of_nat_def ..