diff -r de51a86fc903 -r cc97b347b301 src/HOL/Old_Number_Theory/Fib.thy
--- a/src/HOL/Old_Number_Theory/Fib.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -106,7 +106,7 @@
   apply (case_tac m)
    apply simp 
   apply (simp add: fib_add)
-  apply (simp add: add_commute gcd_non_0 [OF fib_Suc_gr_0])
+  apply (simp add: add.commute gcd_non_0 [OF fib_Suc_gr_0])
   apply (simp add: gcd_non_0 [OF fib_Suc_gr_0, symmetric])
   apply (simp add: gcd_fib_Suc_eq_1 gcd_mult_cancel)
   done