Old application syntax incompatible with Eisbach

1 files changed, 14 insertions, 14 deletions

diff --git a/Sum.thy b/Sum.thy
index 2d6e64b..cdfe5bd 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -22,8 +22,8 @@ syntax
   "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3SUM _:_./ _)" 20)
 
 translations
-  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
-  "SUM x:A. B" \<rightharpoonup> "CONST Sum(A, \<lambda>x. B)"
+  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
+  "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
 
 text "Nondependent pair."
 
@@ -40,25 +40,25 @@ and
 and
   Sum_elim: "\<And>i A B C f p. \<lbrakk>
     C: \<Sum>x:A. B(x) \<longrightarrow> U(i);
-    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x, y) : C((x,y));
+    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
     p : \<Sum>x:A. B(x)
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f, p) : C(p)"  (* What does writing \<lambda>x y. f(x, y) change? *)
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(p) : C(p)"  (* What does writing \<lambda>x y. f(x, y) change? *)
 and
   Sum_comp: "\<And>i A B C f a b. \<lbrakk>
-    A : U(i);
+    A: U(i);
     B: A \<longrightarrow> U(i);
-    C: \<Sum>x:A. B x \<longrightarrow> U(i);
-    \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
-    a : A;
-    b : B a
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f (a,b) \<equiv> f a b"
+    C: \<Sum>x:A. B(x) \<longrightarrow> U(i);
+    \<And>x y. \<lbrakk>x: A; y :B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
+    a: A;
+    b: B(a)
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)((a,b)) \<equiv> f(a)(b)"
 
 text "Admissible inference rules for sum formation:"
 
 axiomatization where
-  Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> A : U(i)"
+  Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
 and
-  Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+  Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 
 lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
 lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2
@@ -69,11 +69,11 @@ section \<open>Empty type\<close>
 
 axiomatization
   Empty :: Term  ("\<zero>") and
-  indEmpty :: "[Typefam, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
+  indEmpty :: "Term \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
 where
   Empty_form: "\<zero> : U(O)"
 and
-  Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z"
+  Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
 
 lemmas Empty_rules [intro] = Empty_form Empty_elim