--- a/src/Pure/Thy/document_output.ML Sat Nov 13 16:43:04 2021 +0100
+++ b/src/Pure/Thy/document_output.ML Sat Nov 13 17:22:10 2021 +0100
@@ -211,8 +211,8 @@
(* command spans *)
-type command = string * Position.T; (*name, position*)
-type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
+type command = string * Position.T; (*name, position*)
+type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
datatype span = Span of command * (source * source * source * source) * bool;