1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -16,12 +16,6 @@
     1.4  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
     1.5  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
     1.6  
     1.7 -primrec
     1.8 -  sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
     1.9 -where
    1.10 -  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    1.11 -| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    1.12 -
    1.13  declare [[map sum = (sum_map, sum_rel)]]
    1.14  
    1.15  

     2.1 --- a/src/HOL/Sum_Type.thy	Thu Nov 18 17:01:16 2010 +0100
     2.2 +++ b/src/HOL/Sum_Type.thy	Thu Nov 18 17:01:16 2010 +0100
     2.3 @@ -91,6 +91,20 @@
     2.4    then show "P s" by (auto intro: sumE [of s])
     2.5  qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
     2.6  
     2.7 +primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
     2.8 +  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
     2.9 +| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    2.10 +
    2.11 +type_mapper sum_map proof -
    2.12 +  fix f g h i s
    2.13 +  show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
    2.14 +    by (cases s) simp_all
    2.15 +next
    2.16 +  fix s
    2.17 +  show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
    2.18 +    by (cases s) simp_all
    2.19 +qed
    2.20 +
    2.21  
    2.22  subsection {* Projections *}
    2.23