diff -r f4be1b0d7a51 -r ef1a18e20ace src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Fri May 21 11:19:53 2021 +0200
+++ b/src/Pure/pure_syn.ML	Fri May 21 12:29:29 2021 +0200
@@ -20,8 +20,8 @@
 fun output_document state markdown txt =
   let
     val ctxt = Toplevel.presentation_context state;
-    val _ = Context_Position.reports ctxt (Thy_Output.document_reports txt);
-  in Thy_Output.output_document ctxt markdown txt end;
+    val _ = Context_Position.reports ctxt (Document_Output.document_reports txt);
+  in Document_Output.output_document ctxt markdown txt end;
 
 fun document_command markdown (loc, txt) =
   Toplevel.keep (fn state =>