diff -r 760e21900b01 -r 28e788ca2c5d src/Doc/Isar_Ref/Proof_Script.thy
--- a/src/Doc/Isar_Ref/Proof_Script.thy	Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy	Thu Oct 22 21:16:49 2015 +0200
@@ -111,7 +111,7 @@
   to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
   y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
   "for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
-  latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
+  latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
   positions may be skipped via dummies (underscore). Unspecified names
   remain internal, and thus inaccessible in the proof text.