diff -r 4b41df5fef81 -r 7435b6a3f72e src/Doc/Tutorial/Inductive/AB.thy
--- a/src/Doc/Tutorial/Inductive/AB.thy	Tue Oct 07 21:44:41 2014 +0200
+++ b/src/Doc/Tutorial/Inductive/AB.thy	Tue Oct 07 22:35:11 2014 +0200
@@ -17,7 +17,7 @@
 B &\to& b S \mid a B B \nonumber
 \end{eqnarray}
 At the end we say a few words about the relationship between
-the original proof \cite[p.\ts81]{HopcroftUllman} and our formal version.
+the original proof @{cite \<open>p.\ts81\<close> HopcroftUllman} and our formal version.
 
 We start by fixing the alphabet, which consists only of @{term a}'s
 and~@{term b}'s:
@@ -283,7 +283,7 @@
 text{*
 We conclude this section with a comparison of our proof with 
 Hopcroft\index{Hopcroft, J. E.} and Ullman's\index{Ullman, J. D.}
-\cite[p.\ts81]{HopcroftUllman}.
+@{cite \<open>p.\ts81\<close> HopcroftUllman}.
 For a start, the textbook
 grammar, for no good reason, excludes the empty word, thus complicating
 matters just a little bit: they have 8 instead of our 7 productions.