src/Doc/Implementation/Integration.thy

--- a/src/Doc/Implementation/Integration.thy	Mon Oct 20 13:29:52 2025 +0200
+++ b/src/Doc/Implementation/Integration.thy	Mon Oct 20 14:38:15 2025 +0200
@@ -150,14 +150,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{define_ML use_thy: "string -> unit"} \\
   @{define_ML Thy_Info.get_theory: "string -> theory"} \\
   @{define_ML Thy_Info.remove_thy: "string -> unit"} \\
   \end{mldecls}
 
-  \<^descr> \<^ML>\<open>use_thy\<close>~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the
-  external file store; outdated ancestors are reloaded on demand.
-
   \<^descr> \<^ML>\<open>Thy_Info.get_theory\<close>~\<open>A\<close> retrieves the theory value presently
   associated with name \<open>A\<close>. Note that the result might be outdated wrt.\ the
   file-system content.