src/Pure/ROOT.ML
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";