--- a/src/Doc/Implementation/Integration.thy Mon Apr 04 15:53:56 2016 +0200
+++ b/src/Doc/Implementation/Integration.thy Mon Apr 04 16:14:22 2016 +0200
@@ -152,7 +152,6 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML use_thy: "string -> unit"} \\
- @{index_ML use_thys: "string list -> unit"} \\[0.5ex]
@{index_ML Thy_Info.get_theory: "string -> theory"} \\
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\
@@ -161,14 +160,6 @@
\<^descr> @{ML use_thy}~\<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 use_thys} is similar to @{ML use_thy}, but handles several theories
- simultaneously. Thus it acts like processing the import header of a theory,
- without performing the merge of the result. By loading a whole sub-graph of
- theories, the intrinsic parallelism can be exploited by the system to
- speedup loading.
-
- This variant is used by default in @{tool build} @{cite "isabelle-system"}.
-
\<^descr> @{ML Thy_Info.get_theory}~\<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 Apr 04 15:53:56 2016 +0200
+++ b/src/Doc/System/Environment.thy Mon Apr 04 16:14:22 2016 +0200
@@ -395,8 +395,8 @@
The user is connected to the raw ML toplevel loop: this is neither
Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
- relevant ML commands at this stage are @{ML use}, @{ML use_thy}, @{ML
- use_thys}.
+ relevant ML commands at this stage are @{ML use} (for ML files) and
+ @{ML use_thy} (for theory files).
\<close>
--- a/src/Pure/ML/ml_final.ML Mon Apr 04 15:53:56 2016 +0200
+++ b/src/Pure/ML/ml_final.ML Mon Apr 04 16:14:22 2016 +0200
@@ -12,10 +12,6 @@
structure Pure = struct val thy = Thy_Info.pure_theory () end;
-fun use_thys args =
- Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
-val use_thy = use_thys o single;
-
Proofterm.proofs := 0;
Context.set_thread_data NONE;
--- a/src/Pure/ROOT.ML Mon Apr 04 15:53:56 2016 +0200
+++ b/src/Pure/ROOT.ML Mon Apr 04 16:14:22 2016 +0200
@@ -321,7 +321,7 @@
use "Tools/named_thms.ML";
use "ML/ml_pp.ML";
use "ML/ml_file.ML";
-Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
+use_thy "Pure";
(* final ML setup *)
--- a/src/Pure/Thy/thy_info.ML Mon Apr 04 15:53:56 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Apr 04 16:14:22 2016 +0200
@@ -388,3 +388,5 @@
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, Position.none));