--- 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>