diff -r 9c50eb3bff50 -r ddb3ac3fef45 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Nov 04 18:14:28 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Nov 04 18:32:47 2015 +0100
@@ -530,8 +530,8 @@
 
   \<^medskip>
   The Isar calculation proof commands may be defined as
-  follows:\footnote{We suppress internal bookkeeping such as proper
-  handling of block-structure.}
+  follows:\<^footnote>\<open>We suppress internal bookkeeping such as proper
+  handling of block-structure.\<close>
 
   \begin{matharray}{rcl}
     @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
@@ -718,9 +718,9 @@
   If the goal had been \<open>show\<close> (or \<open>thus\<close>), some
   pending sub-goal is solved as well by the rule resulting from the
   result \<^emph>\<open>exported\<close> into the enclosing goal context.  Thus \<open>qed\<close> may fail for two reasons: either \<open>m\<^sub>2\<close> fails, or the
-  resulting rule does not fit to any pending goal\footnote{This
+  resulting rule does not fit to any pending goal\<^footnote>\<open>This
   includes any additional ``strong'' assumptions as introduced by
-  @{command "assume"}.} of the enclosing context.  Debugging such a
+  @{command "assume"}.\<close> of the enclosing context.  Debugging such a
   situation might involve temporarily changing @{command "show"} into
   @{command "have"}, or weakening the local context by replacing
   occurrences of @{command "assume"} by @{command "presume"}.