src/Pure/Thy/document_output.ML
changeset 74838 4c8d9479f916
parent 74835 26c3a9c92e11
child 74882 947bb3e09a88
--- a/src/Pure/Thy/document_output.ML	Tue Nov 23 21:43:45 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Wed Nov 24 15:33:43 2021 +0100
@@ -8,7 +8,7 @@
 sig
   val document_reports: Input.source -> Position.report list
   val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text
-  val document_output: {markdown: bool, markup: Position.T -> Latex.text -> Latex.text} ->
+  val document_output: {markdown: bool, markup: Latex.text -> Latex.text} ->
     (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val output_token: Proof.context -> Token.T -> Latex.text
@@ -119,7 +119,7 @@
       let
         val ctxt = Toplevel.presentation_context st;
         val _ = Context_Position.reports ctxt (document_reports txt);
-      in txt |> output_document ctxt {markdown = markdown} |> markup (Position.thread_data ()) end;
+      in txt |> output_document ctxt {markdown = markdown} |> markup end;
   in
     Toplevel.present (fn st =>
       (case loc of