1.1 --- a/src/HOL/Sum_Type.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
     1.5    "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
     1.6  
     1.7 -typedef (sum) ('a, 'b) "+" (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
     1.8 +typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
     1.9    by auto
    1.10  
    1.11  lemma Inl_RepI: "Inl_Rep a \<in> sum"
    1.12 @@ -83,7 +83,7 @@
    1.13    with assms show P by (auto simp add: sum_def Inl_def Inr_def)
    1.14  qed
    1.15  
    1.16 -rep_datatype (sum) Inl Inr
    1.17 +rep_datatype Inl Inr
    1.18  proof -
    1.19    fix P
    1.20    fix s :: "'a + 'b"