diff -r 1dd29afaddda -r f7f8bb1c28ce src/Doc/Implementation/Integration.thy
--- a/src/Doc/Implementation/Integration.thy	Sun Jun 01 16:43:09 2025 +0200
+++ b/src/Doc/Implementation/Integration.thy	Sun Jun 01 17:06:33 2025 +0200
@@ -153,7 +153,6 @@
   @{define_ML use_thy: "string -> unit"} \\
   @{define_ML Thy_Info.get_theory: "string -> theory"} \\
   @{define_ML Thy_Info.remove_thy: "string -> unit"} \\
-  @{define_ML Thy_Info.register_thy: "theory -> 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
@@ -165,10 +164,6 @@
 
   \<^descr> \<^ML>\<open>Thy_Info.remove_thy\<close>~\<open>A\<close> deletes theory \<open>A\<close> and all descendants from
   the theory database.
-
-  \<^descr> \<^ML>\<open>Thy_Info.register_thy\<close>~\<open>text thy\<close> registers an existing theory value
-  with the theory loader database and updates source version information
-  according to the file store.
 \<close>
 
 end