# HG changeset patch
# User wenzelm
# Date 1511947676 -3600
# Node ID 05ff3e6dbbce8566479a82feb98bb22e2a2ab2d7
# Parent  a2fa0c6a7aff4cd791e47393def302e345d4c18a
clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;

diff -r a2fa0c6a7aff -r 05ff3e6dbbce src/Pure/ML_Bootstrap.thy
--- 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>
diff -r a2fa0c6a7aff -r 05ff3e6dbbce src/Pure/Pure.thy
--- 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>