src/Pure/ML/ml_file.ML
changeset 73761 ef1a18e20ace
parent 72747 5f9d66155081
child 78035 bd5f6cee8001
--- a/src/Pure/ML/ml_file.ML	Fri May 21 11:19:53 2021 +0200
+++ b/src/Pure/ML/ml_file.ML	Fri May 21 12:29:29 2021 +0200
@@ -21,7 +21,7 @@
     val provide = Resources.provide_file file;
     val source = Token.file_source file;
 
-    val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
+    val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
 
     val flags: ML_Compiler.flags =
       {environment = environment, redirect = true, verbose = true,