diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -18,9 +18,8 @@
 imports "../Number_Theory/Primes"
 begin
 
-text_raw \<open>\footnote{Isar version by Gertrud Bauer.  Original tactic
-  script by Larry Paulson.  A few proofs of laws taken from
-  @{cite "Concrete-Math"}.}\<close>
+text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
+  Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
 
 
 declare One_nat_def [simp]