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,