# HG changeset patch # User wenzelm # Date 1635413869 -7200 # Node ID c6610137a092e6b749e6b73321190709748f0017 # Parent eceb93181ad9c303ce39e60e9151184e431cdfb7 tuned modules; diff -r eceb93181ad9 -r c6610137a092 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Oct 27 20:07:13 2021 +0200 +++ b/src/Pure/ROOT.ML Thu Oct 28 11:37:49 2021 +0200 @@ -303,7 +303,6 @@ (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; -ML_file "ML/ml_pid.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/document_output.ML"; ML_file "Thy/document_antiquotations.ML"; @@ -319,6 +318,13 @@ ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; +(*ML add-ons*) +ML_file "ML/ml_pp.ML"; +ML_file "ML/ml_thms.ML"; +ML_file "ML/ml_instantiate.ML"; +ML_file "ML/ml_file.ML"; +ML_file "ML/ml_pid.ML"; + (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; @@ -337,11 +343,6 @@ subsection "Miscellaneous tools and packages for Pure Isabelle"; -ML_file "ML/ml_pp.ML"; -ML_file "ML/ml_thms.ML"; -ML_file "ML/ml_instantiate.ML"; -ML_file "ML/ml_file.ML"; - ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML";