src/Pure/ROOT.ML
changeset 70396 425c5f9bc61a
parent 70364 b2bedb022a75
child 70443 a21a96eda033
--- a/src/Pure/ROOT.ML	Mon Jul 22 14:47:21 2019 +0200
+++ b/src/Pure/ROOT.ML	Mon Jul 22 16:15:40 2019 +0200
@@ -129,6 +129,7 @@
 ML_file "Concurrent/cache.ML";
 
 ML_file "PIDE/active.ML";
+ML_file "Thy/export.ML";
 
 
 subsection "Inner syntax";
@@ -305,7 +306,6 @@
 ML_file "PIDE/command.ML";
 ML_file "PIDE/query_operation.ML";
 ML_file "PIDE/resources.ML";
-ML_file "Thy/export.ML";
 ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
 ML_file "Thy/export_theory.ML";