--- 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 =>