src/HOL/Sum_Type.thy

 lemmas cases = sum.case
 lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
 
 setup {* Sign.parent_path *}
 
-primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
+old_primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
 functor sum_map: sum_map proof -
   fix f g h i

     from a have "case_sum f1 f2 (Inr y) = case_sum g1 g2 (Inr y)" by simp
     then show "f2 y = g2 y" by simp
   qed
 qed
 
-primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
+old_primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   "Suml f (Inl x) = f x"
 
-primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
+old_primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
   "Sumr f (Inr x) = f x"
 
 lemma Suml_inject:
   assumes "Suml f = Suml g" shows "f = g"
 proof