diff -r de51a86fc903 -r cc97b347b301 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -60,7 +60,7 @@
 lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
   apply (induct n rule: fib.induct)
   apply auto
-  apply (metis gcd_add1_nat nat_add_commute)
+  apply (metis gcd_add1_nat add.commute)
   done
 
 lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
@@ -68,7 +68,7 @@
   apply (cases m)
   apply (auto simp add: fib_add)
   apply (subst gcd_commute_nat)
-  apply (subst mult_commute)
+  apply (subst mult.commute)
   apply (metis coprime_fib_Suc_nat gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
   done