diff -r bda7527ccf05 -r cc2d676d5395 src/HOL/IMP/Compiler2.thy
--- a/src/HOL/IMP/Compiler2.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/HOL/IMP/Compiler2.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -8,7 +8,7 @@
 
 text \<open>
 The preservation of the source code semantics is already shown in the 
-parent theory @{text "Compiler"}. This here shows the second direction.
+parent theory \<open>Compiler\<close>. This here shows the second direction.
 \<close>
 
 subsection \<open>Definitions\<close>