1.1 --- a/src/HOL/RealDef.thy	Fri Feb 15 13:54:54 2013 +0100
     1.2 +++ b/src/HOL/RealDef.thy	Fri Feb 15 15:22:16 2013 +0100
     1.3 @@ -987,6 +987,7 @@
     1.4  declare [[coercion "int"]]
     1.5  
     1.6  declare [[coercion_map map]]
     1.7 +declare [[coercion_map image]]
     1.8  declare [[coercion_map "% f g h x. g (h (f x))"]]
     1.9  declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
    1.10