# HG changeset patch
# User wenzelm
# Date 1748790393 -7200
# Node ID f7f8bb1c28cede7bf08bf7baf59dd35ae2860b53
# Parent  1dd29afadddad841c643e36f4c600b9bb2d5231f
obsolete (see 22d65e375c01);

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
diff -r 1dd29afaddda -r f7f8bb1c28ce src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jun 01 16:43:09 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 01 17:06:33 2025 +0200
@@ -26,7 +26,6 @@
     (theory * Document_Output.segment list) list
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
-  val register_thy: theory -> unit
   val finish: unit -> unit
 end;
 
@@ -471,22 +470,6 @@
   in Toplevel.end_theory end_pos end_state end;
 
 
-(* register theory *)
-
-fun register_thy theory =
-  let
-    val name = Context.theory_long_name theory;
-    val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
-    val imports = Resources.imports_of theory;
-  in
-    change_thys (fn thys =>
-      let
-        val thys' = remove name thys;
-        val _ = writeln ("Registering theory " ^ quote name);
-      in update (make_deps master imports) (theory, []) thys' end)
-  end;
-
-
 (* finish all theories *)
 
 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));