diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Advanced/WFrec.thy
--- a/src/Doc/Tutorial/Advanced/WFrec.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Advanced/WFrec.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -29,7 +29,7 @@
 left-hand side of an equation and $r$ the argument of some recursive call on
 the corresponding right-hand side, induces a well-founded relation.  For a
 systematic account of termination proofs via well-founded relations see, for
-example, Baader and Nipkow~\cite{Baader-Nipkow}.
+example, Baader and Nipkow~@{cite "Baader-Nipkow"}.
 
 Each \isacommand{recdef} definition should be accompanied (after the function's
 name) by a well-founded relation on the function's argument type.