src/Doc/antiquote_setup.ML
changeset 59066 45ab32a542fe
parent 59064 a8bcb5a446c8
child 59067 dd8ec9138112
--- a/src/Doc/antiquote_setup.ML	Sun Nov 30 12:46:16 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
@@ -69,7 +69,7 @@
   | _ => error ("Single ML name expected in input: " ^ quote txt));
 
 fun prep_ml source =
-  (#1 (Input.source_content source), ML_Lex.read_source false source);
+  (Input.source_content source, ML_Lex.read_source false source);
 
 fun index_ml name kind ml = Thy_Output.antiquotation name
   (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))