diff -r 1884c40f1539 -r e467ae7aa808 src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Sun Oct 18 21:30:01 2015 +0200
+++ b/src/Doc/Implementation/Integration.thy	Sun Oct 18 22:57:09 2015 +0200
@@ -9,7 +9,7 @@
 section \<open>Isar toplevel \label{sec:isar-toplevel}\<close>
 
 text \<open>
-  The Isar \emph{toplevel state} represents the outermost configuration that
+  The Isar \<^emph>\<open>toplevel state\<close> represents the outermost configuration that
   is transformed by a sequence of transitions (commands) within a theory body.
   This is a pure value with pure functions acting on it in a timeless and
   stateless manner. Historically, the sequence of transitions was wrapped up
@@ -149,8 +149,8 @@
   In batch mode and within dumped logic images, the theory database maintains
   a collection of theories as a directed acyclic graph. A theory may refer to
   other theories as @{keyword "imports"}, or to auxiliary files via special
-  \emph{load commands} (e.g.\ @{command ML_file}). For each theory, the base
-  directory of its own theory file is called \emph{master directory}: this is
+  \<^emph>\<open>load commands\<close> (e.g.\ @{command ML_file}). For each theory, the base
+  directory of its own theory file is called \<^emph>\<open>master directory\<close>: this is
   used as the relative location to refer to other files from that theory.
 \<close>