changeset 73761 | ef1a18e20ace |
parent 73613 | c1d8cd6d1a49 |
child 73834 | 364bac6691de |
--- a/src/Pure/ROOT.ML Fri May 21 11:19:53 2021 +0200 +++ b/src/Pure/ROOT.ML Fri May 21 12:29:29 2021 +0200 @@ -304,7 +304,7 @@ ML_file "ML/ml_antiquotations2.ML"; ML_file "ML/ml_pid.ML"; ML_file "Thy/document_antiquotation.ML"; -ML_file "Thy/thy_output.ML"; +ML_file "Thy/document_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML";