--- a/QuotScript.thy	Wed Oct 28 17:38:37 2009 +0100
+++ b/QuotScript.thy	Wed Oct 28 18:08:38 2009 +0100
@@ -131,9 +131,9 @@
   "FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
 
 abbreviation
-  FUN_REL_syn ("_ ===> _")
+  FUN_REL_syn (infixr "===>" 55)
 where
-  "E1 ===> E2 \<equiv> FUN_REL E1 E2"  
+  "E1 ===> E2 \<equiv> FUN_REL E1 E2"
 
 lemma FUN_REL_EQ:
   "(op =) ===> (op =) = (op =)"
@@ -512,11 +512,11 @@
 
 (* These are the fixed versions, general ones need to be proved. *)
 lemma ho_all_prs:
-  shows "op = ===> op = ===> op = All All"
+  shows "((op = ===> op =) ===> op =) All All"
   by auto
 
-lemma ho_ex_prs: 
-  shows "op = ===> op = ===> op = Ex Ex"
+lemma ho_ex_prs:
+  shows "((op = ===> op =) ===> op =) Ex Ex"
   by auto
 
 end