1 files changed, 4 insertions, 4 deletions
diff --git a/Coprod.thy b/Coprod.thy
index 1ff7361..97e0566 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -12,10 +12,10 @@ begin
 section \<open>Constants and type rules\<close>
 
 axiomatization
-  Coprod :: "[Term, Term] \<Rightarrow> Term"  (infixr "+" 50) and
-  inl :: "Term \<Rightarrow> Term" and
-  inr :: "Term \<Rightarrow> Term" and
-  indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>+)")
+  Coprod :: "[t, t] \<Rightarrow> t"  (infixr "+" 50) and
+  inl :: "t \<Rightarrow> t" and
+  inr :: "t \<Rightarrow> t" and
+  indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>+)")
 where
   Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i"
 and