changeset 70893 | ce1e27dcc9f4 |
parent 70784 | 799437173553 |
child 70907 | 7e3f25a0cee4 |
--- a/src/Pure/ROOT.ML Thu Oct 17 17:24:13 2019 +0200 +++ b/src/Pure/ROOT.ML Thu Oct 17 20:28:31 2019 +0200 @@ -310,7 +310,7 @@ ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; -ML_file "Thy/thm_deps.ML"; +ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML";