# HG changeset patch
# User wenzelm
# Date 1459779262 -7200
# Node ID 1bd1d84929316e635a5db5302c5ef87cc9494f43
# Parent  3c576c7f97313998290d62e9adbbd6783e4b7f75
clarified bootstrap;

diff -r 3c576c7f9731 -r 1bd1d8492931 src/Doc/Implementation/Integration.thy
--- 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.
diff -r 3c576c7f9731 -r 1bd1d8492931 src/Doc/System/Environment.thy
--- 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>
 
 
diff -r 3c576c7f9731 -r 1bd1d8492931 src/Pure/ML/ml_final.ML
--- 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;
diff -r 3c576c7f9731 -r 1bd1d8492931 src/Pure/ROOT.ML
--- 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 *)
diff -r 3c576c7f9731 -r 1bd1d8492931 src/Pure/Thy/thy_info.ML
--- 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));