1 files changed, 1 insertions, 1 deletions
diff --git a/HoTT.thy b/HoTT.thy
index c1c6e72..44f55e9 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -57,7 +57,7 @@ translations
   "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
   (* The above syntax translations bind the x in the expressions B, b. *)
 
-abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 80)
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
   where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
 
 axiomatization