--- a/src/Pure/Thy/thy_output.ML Sat Nov 07 15:23:26 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Nov 07 16:05:28 2015 +0100
@@ -196,10 +196,7 @@
fun output_text state {markdown} source =
let
val pos = Input.pos_of source;
- val _ =
- Position.report pos
- (Markup.language_document
- {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
+ val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
val syms = Input.source_explode source;
val output_antiquotes = map (eval_antiquote state) #> implode;