# HG changeset patch
# User wenzelm
# Date 1511794764 -3600
# Node ID d1b8464654c5ba814a5ef6380bc0426df494b30f
# Parent  e77f13a6a50107ddb51bc5e3e7eb1bd3ded17791
retain files in Pure.thy, notably $POLYML_EXE;

diff -r e77f13a6a501 -r d1b8464654c5 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Nov 27 11:45:20 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Nov 27 15:59:24 2017 +0100
@@ -238,8 +238,9 @@
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
-                  (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
-                    dependencies.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
+                  val pure_files = resources.pure_files(overall_syntax, info.dir)
+                  dependencies.loaded_files.map({ case (name, files) =>
+                    (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
                 }
                 else dependencies.loaded_files
               }