# HG changeset patch
# User noschinl
# Date 1301062929 -3600
# Node ID 9cb122742f5c37d8b70b0be38b3fdfb315afee29
# Parent  d1c761375a750ebda695f352077acadf3e1bacf1
Change coercion for RealDef to use function application (not composition)

diff -r d1c761375a75 -r 9cb122742f5c src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Mar 25 11:19:01 2011 +0100
+++ b/src/HOL/RealDef.thy	Fri Mar 25 15:22:09 2011 +0100
@@ -1115,7 +1115,7 @@
 declare [[coercion "int"]]
 
 declare [[coercion_map map]]
-declare [[coercion_map "% f g h . g o h o f"]]
+declare [[coercion_map "% f g h x. g (h (f x))"]]
 declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
 
 lemma real_eq_of_nat: "real = of_nat"