# HG changeset patch
# User wenzelm
# Date 1415788767 -3600
# Node ID 584077922200d7fb04ffe6dee37f99a7f19f4b81
# Parent  92b6f4e68c5a216181b70df7171c858b45e8ae8e
make SML/NJ happy;

diff -r 92b6f4e68c5a -r 584077922200 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Nov 12 10:30:59 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Nov 12 11:39:27 2014 +0100
@@ -195,7 +195,7 @@
     val _ = Position.reports (maps words ants);
   in implode (map expand ants) end;
 
-fun check_text {delimited, text, range} state =
+fun check_text ({delimited, text, range}: Symbol_Pos.source) state =
  (Position.report (fst range) (Markup.language_document delimited);
   if Toplevel.is_skipped_proof state then ()
   else ignore (eval_antiquote state (text, fst range)));