diff -r c9a1caf218c8 -r d5a6096b94ad src/HOL/NewNumberTheory/Cong.thy
--- a/src/HOL/NewNumberTheory/Cong.thy	Wed Jun 24 15:51:07 2009 +0200
+++ b/src/HOL/NewNumberTheory/Cong.thy	Wed Jun 24 17:50:49 2009 +0200
@@ -60,9 +60,7 @@
 lemma nat_1' [simp]: "nat 1 = 1"
 by simp
 
-(* For those annoying moments where Suc reappears *)
-lemma Suc_remove: "Suc n = n + 1"
-by simp
+(* For those annoying moments where Suc reappears, use Suc_eq_plus1 *)
 
 declare nat_1 [simp del]
 declare add_2_eq_Suc [simp del]