diff -r 5ded95dda5df -r 78943ac46f6d src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Sun Oct 28 13:18:00 2007 +0100
+++ b/src/HOL/NumberTheory/Fib.thy	Mon Oct 29 10:37:09 2007 +0100
@@ -43,7 +43,7 @@
 next
   case 2 show ?case  by (simp add: fib_2)
 next
-  case 3 thus ?case by (simp add: fib_2 add_mult_distrib2)
+  case fib_2 thus ?case by (simp add: fib.simps add_mult_distrib2)
 qed
 
 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
@@ -72,9 +72,9 @@
 next
   case 2 thus ?case by (simp add: fib_2 mod_Suc)
 next 
-  case (3 x) 
+  case (fib_2 x) 
   have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
-  with "3.hyps" show ?case by (simp add: fib_2 add_mult_distrib add_mult_distrib2)
+  with "fib_2.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
 qed
 
 text{*We now obtain a version for the natural numbers via the coercion