--- 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);