diff -r dc311d55ad8f -r 6e1e8b5abbfa src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/Code_Test.thy	Fri Aug 12 17:53:55 2016 +0200
@@ -53,9 +53,10 @@
   and (Scala) "_.mkString(\"\")"
 
 text \<open>
-  Stripped-down implementations of Isabelle's XML tree with YXML encoding
-  as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
-  sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
+  Stripped-down implementations of Isabelle's XML tree with YXML encoding as
+  defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
+  sufficient to encode @{typ "Code_Evaluation.term"} as in
+  \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
 \<close>
 
 datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
@@ -113,8 +114,8 @@
 where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
 
 text \<open>
-  Encoding @{typ Code_Evaluation.term} into XML trees
-  as defined in @{file "~~/src/Pure/term_xml.ML"}
+  Encoding @{typ Code_Evaluation.term} into XML trees as defined in
+  \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
 \<close>
 
 definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"