Application should bind tighter than composition

1 files changed, 1 insertions, 1 deletions

diff --git a/Prod.thy b/Prod.thy
index a37fdd6..8d840bd 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -17,7 +17,7 @@ section \<open>Basic definitions\<close>
 axiomatization
   Prod   :: "[t, tf] \<Rightarrow> t" and
   lambda :: "(t \<Rightarrow> t) \<Rightarrow> t"  (binder "\<^bold>\<lambda>" 30) and
-  appl   :: "[t, t] \<Rightarrow> t"  (infixl "`" 105)  \<comment> \<open>Application binds tighter than abstraction.\<close>
+  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`_)" [120, 121] 120)  \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
   "_prod" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Prod>_: _./ _)" 30)