diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Library/Tree_Real.thy
--- a/src/HOL/Library/Tree_Real.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Tree_Real.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -7,8 +7,8 @@
 begin
 
 text \<open>
-  This theory is separate from @{theory "HOL-Library.Tree"} because the former is discrete and
-  builds on @{theory Main} whereas this theory builds on @{theory Complex_Main}.
+  This theory is separate from \<^theory>\<open>HOL-Library.Tree\<close> because the former is discrete and
+  builds on \<^theory>\<open>Main\<close> whereas this theory builds on \<^theory>\<open>Complex_Main\<close>.
 \<close>