diff -r 423202f05a43 -r 7975676c08c0 src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Sun Oct 05 22:46:20 2014 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Sun Oct 05 22:47:07 2014 +0200
@@ -90,7 +90,7 @@
   reset to the target context.  The target now holds definitions for
   terms and theorems that stem from the hypothetical @{text
   "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
-  particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
+  particular target policy (see @{cite \<open>\S4--5\<close> "Haftmann-Wenzel:2009"}
   for details).  *}
 
 text %mlref {*
@@ -159,7 +159,7 @@
 text {*
   %FIXME
 
-  See also \cite{Chaieb-Wenzel:2007}.
+  See also @{cite "Chaieb-Wenzel:2007"}.
 *}
 
 end