diff -r 39be26d1bc28 -r bc7982c54e37 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 26 11:34:17 2010 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Mon Apr 26 11:34:19 2010 +0200
@@ -143,9 +143,9 @@
   apply (induct n rule: fib_induct_nat)
   apply auto
   apply (subst fib_reduce_nat)
-  apply (auto simp add: ring_simps)
+  apply (auto simp add: field_simps)
   apply (subst (1 3 5) fib_reduce_nat)
-  apply (auto simp add: ring_simps Suc_eq_plus1)
+  apply (auto simp add: field_simps Suc_eq_plus1)
 (* hmmm. Why doesn't "n + (1 + (1 + k))" simplify to "n + k + 2"? *)
   apply (subgoal_tac "n + (k + 2) = n + (1 + (1 + k))")
   apply (erule ssubst) back back
@@ -184,7 +184,7 @@
 lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) - 
     (fib (int n + 1))^2 = (-1)^(n + 1)"
   apply (induct n)
-  apply (auto simp add: ring_simps power2_eq_square fib_reduce_int
+  apply (auto simp add: field_simps power2_eq_square fib_reduce_int
       power_add)
 done
 
@@ -222,7 +222,7 @@
   apply (subst (2) fib_reduce_nat)
   apply (auto simp add: Suc_eq_plus1) (* again, natdiff_cancel *)
   apply (subst add_commute, auto)
-  apply (subst gcd_commute_nat, auto simp add: ring_simps)
+  apply (subst gcd_commute_nat, auto simp add: field_simps)
 done
 
 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
@@ -305,7 +305,7 @@
 theorem fib_mult_eq_setsum_nat:
     "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
   apply (induct n)
-  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat ring_simps)
+  apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
 done
 
 theorem fib_mult_eq_setsum'_nat: