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";