src/HOL/Sum_Type.thy

   "Inl_Rep a x y p \<longleftrightarrow> x = a \<and> p"
 
 definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
   "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
 
-typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
+typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
   by auto
 
 lemma Inl_RepI: "Inl_Rep a \<in> sum"
   by (auto simp add: sum_def)
 

   fix f 
   assume "s = Abs_sum f" and "f \<in> sum"
   with assms show P by (auto simp add: sum_def Inl_def Inr_def)
 qed
 
-rep_datatype (sum) Inl Inr
+rep_datatype Inl Inr
 proof -
   fix P
   fix s :: "'a + 'b"
   assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
   then show "P s" by (auto intro: sumE [of s])