--- a/QuotScript.thy	Fri Oct 16 10:54:31 2009 +0200
+++ b/QuotScript.thy	Fri Oct 16 16:51:01 2009 +0200
@@ -103,17 +103,18 @@
   "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
 
 fun
-  fun_map 
+  fun_map
 where
   "fun_map f g h x = g (h (f x))"
 
+
 abbreviation
-  fun_map_syn ("_ ---> _")
+  fun_map_syn (infixr "--->" 55)
 where
-  "f ---> g \<equiv> fun_map f g"  
+  "f ---> g \<equiv> fun_map f g"
 
 lemma FUN_MAP_I:
-  shows "(\<lambda>x. x ---> \<lambda>x. x) = (\<lambda>x. x)"
+  shows "((\<lambda>x. x) ---> (\<lambda>x. x)) = (\<lambda>x. x)"
 by (simp add: expand_fun_eq)
 
 lemma IN_FUN: