
diff -r 4d5fbec92bb1 -r 25271ff79171 src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Fri Feb 26 18:33:01 2016 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Fri Feb 26 22:15:09 2016 +0100
@@ -80,7 +80,7 @@
   also have "\<dots> = fib (n + 2) + fib (n + 1)"
     by simp
   also have "gcd (fib (n + 2)) \<dots> = gcd (fib (n + 2)) (fib (n + 1))"
-    by (rule gcd_add2_nat)
+    by (rule gcd_add2)
   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd.commute)
   also assume "\<dots> = 1"




