diff -r 7a2c567061b3 -r aa99568f56de src/HOL/SPARK/Manual/VC_Principles.thy
--- a/src/HOL/SPARK/Manual/VC_Principles.thy	Tue Oct 07 22:54:49 2014 +0200
+++ b/src/HOL/SPARK/Manual/VC_Principles.thy	Tue Oct 07 23:12:08 2014 +0200
@@ -76,7 +76,7 @@
 \caption{Control flow graph for procedure \texttt{Proc2}}
 \label{fig:proc2-graph}
 \end{figure}
-As explained by Barnes \cite[\S 11.5]{Barnes}, the \SPARK{} Examiner unfolds the loop
+As explained by Barnes @{cite \<open>\S 11.5\<close> Barnes}, the \SPARK{} Examiner unfolds the loop
 \begin{lstlisting}
 for I in T range L .. U loop
   --# assert P (I);