diff -r dc311d55ad8f -r 6e1e8b5abbfa src/Doc/Implementation/Eq.thy
--- a/src/Doc/Implementation/Eq.thy	Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Eq.thy	Fri Aug 12 17:53:55 2016 +0200
@@ -64,10 +64,10 @@
   @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
   \end{mldecls}
 
-  See also @{file "~~/src/Pure/thm.ML" } for further description of these
-  inference rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note
-  that \<open>\<alpha>\<close> conversion is implicit due to the representation of terms with
-  de-Bruijn indices (\secref{sec:terms}).
+  See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
+  rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
+  conversion is implicit due to the representation of terms with de-Bruijn
+  indices (\secref{sec:terms}).
 \<close>