diff -r dc311d55ad8f -r 6e1e8b5abbfa src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Logic.thy	Fri Aug 12 17:53:55 2016 +0200
@@ -1248,11 +1248,11 @@
 \<close>
 
 text %mlex \<open>
-  \<^item> @{file "~~/src/HOL/Proofs/ex/Proof_Terms.thy"} provides basic examples
-  involving proof terms.
+  \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close> provides basic examples involving
+  proof terms.
 
-  \<^item> @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} demonstrates export and import
-  of proof terms via XML/ML data representation.
+  \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/XML_Data.thy\<close> demonstrates export and import of
+  proof terms via XML/ML data representation.
 \<close>
 
 end