diff -r e7d4dac7a79f -r 26c76e143b77 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Nov 04 11:53:22 2015 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Nov 04 14:40:18 2015 +0100
@@ -145,8 +145,8 @@
 
 text \<open>See @{file "~~/src/HOL/ROOT"} for a diversity of practically
   relevant situations, although it uses relatively complex
-  quasi-hierarchic naming conventions like \<open>HOL\<dash>SPARK\<close>,
-  \<open>HOL\<dash>SPARK\<dash>Examples\<close>.  An alternative is to use
+  quasi-hierarchic naming conventions like \<^verbatim>\<open>HOL-SPARK\<close>,
+  \<^verbatim>\<open>HOL-SPARK-Examples\<close>.  An alternative is to use
   unqualified names that are relatively long and descriptive, as in
   the Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
   example.\<close>