clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
--- a/src/Pure/ML_Bootstrap.thy Tue Nov 28 22:14:10 2017 +0100
+++ b/src/Pure/ML_Bootstrap.thy Wed Nov 29 10:27:56 2017 +0100
@@ -8,6 +8,9 @@
imports Pure
begin
+external_file "$POLYML_EXE"
+
+
subsection \<open>Standard ML environment for virtual bootstrap\<close>
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
--- a/src/Pure/Pure.thy Tue Nov 28 22:14:10 2017 +0100
+++ b/src/Pure/Pure.thy Wed Nov 29 10:27:56 2017 +0100
@@ -120,8 +120,6 @@
in () end)));
\<close>
-external_file "$POLYML_EXE"
-
subsection \<open>Embedded ML text\<close>