diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/Sum_Type.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -114,9 +114,8 @@
 
 lemmas induct = old.sum.induct
 lemmas inducts = old.sum.inducts
-lemmas recs = old.sum.recs
-lemmas cases = sum.case
-lemmas simps = sum.inject sum.distinct sum.case old.sum.recs
+lemmas rec = old.sum.rec
+lemmas simps = sum.inject sum.distinct sum.case sum.rec
 
 setup {* Sign.parent_path *}