discontinue ancient "use_thy" operation: does not quite work without Isabelle/Scala session context;

--- a/NEWS	Mon Oct 20 13:29:52 2025 +0200
+++ b/NEWS	Mon Oct 20 14:38:15 2025 +0200
@@ -382,6 +382,13 @@
 
   isabelle process_theories -f '~~/src/HOL/Examples/Seq.thy'
 
+* The command-line tool "isabelle process" no longer supports option -T
+to load individual theories via the "use_thy" function in Isabelle/ML.
+The latter is still available as "Thy_Info.use_thy_legacy", notably for
+"isabelle process -e ...", but it will be removed eventually. The proper
+way to process individual theories under program control is via
+"isabelle process_theories". INCOMPATIBILITY.
+
 * System option "show_results" (default true) controls output of
 toplevel command results (definitions, theorems) in batch-builds. In
 interactive mode this is always enabled; in batch-builds it can be

--- 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.

--- a/src/Doc/System/Environment.thy	Mon Oct 20 13:29:52 2025 +0200
+++ b/src/Doc/System/Environment.thy	Mon Oct 20 14:38:15 2025 +0200
@@ -325,7 +325,6 @@
 \<open>Usage: isabelle process [OPTIONS]
 
   Options are:
-    -T THEORY    load theory
     -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
@@ -342,10 +341,6 @@
   a premature exit of the ML process with return code 1.
 
   \<^medskip>
-  Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with
-  a suitable \<^ML>\<open>use_thy\<close> invocation.
-
-  \<^medskip>
   Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
   additional directories for session roots, see also \secref{sec:tool-build}.
 

--- a/src/Pure/ML/ml_process.scala	Mon Oct 20 13:29:52 2025 +0200
+++ b/src/Pure/ML/ml_process.scala	Mon Oct 20 14:38:15 2025 +0200
@@ -143,7 +143,6 @@
 Usage: isabelle process [OPTIONS]
 
   Options are:
-    -T THEORY    load theory
     -d DIR       include session directory
     -e ML_EXPR   evaluate ML expression on startup
     -f ML_FILE   evaluate ML file on startup
@@ -153,8 +152,6 @@
 
   Run the raw Isabelle ML process in batch mode.
 """,
-        "T:" -> (arg =>
-          eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
         "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),

--- a/src/Pure/Thy/thy_info.ML	Mon Oct 20 13:29:52 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Oct 20 14:38:15 2025 +0200
@@ -24,7 +24,7 @@
   val remove_thy: string -> unit
   val use_theories: Options.T -> string -> (string * Position.T) list ->
     (theory * Document_Output.segment list) list
-  val use_thy: string -> unit
+  val use_thy_legacy: string -> unit
   val finish: unit -> unit
 end;
 
@@ -458,8 +458,9 @@
 fun use_theories options qualifier imports =
   schedule_theories (#2 (require_thys options [] qualifier Path.current imports String_Graph.empty));
 
-fun use_thy name =
-  ignore (use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]);
+fun use_thy_legacy name =
+  Runtime.toplevel_program (fn () =>
+    ignore (use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]));
 
 
 (* finish all theories *)
@@ -467,5 +468,3 @@
 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
 
 end;
-
-fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);