diff -r 950e1cfe0fe4 -r aedd11603fb4 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Nov 08 12:07:39 2019 +0100 +++ b/src/Pure/ROOT.ML Fri Nov 08 16:11:09 2019 +0100 @@ -111,6 +111,7 @@ subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; +ML_file_no_debug "ML/exn_debugger.ML"; ML_file "ML/ml_statistics.ML"; @@ -199,7 +200,6 @@ ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; -ML_file_no_debug "ML/exn_debugger.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML";