# HG changeset patch
# User wenzelm
# Date 1445264761 -7200
# Node ID 391814730b40d36ed67bfb5c354d74552fb32e1e
# Parent  078ec7b710abb81dfeb39900c4bd1b90e0848e16
tuned;

diff -r 078ec7b710ab -r 391814730b40 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Mon Oct 19 00:19:19 2015 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Oct 19 16:26:01 2015 +0200
@@ -328,10 +328,11 @@
       |> Source.source Symbol_Pos.stopper
         (Scan.recover (Scan.bulk (!!! "bad input" scan))
           (fn msg => recover msg >> map Antiquote.Text))
-      |> Source.exhaust
-      |> tap (Position.reports o Antiquote.antiq_reports)
-      |> tap (Position.reports_text o maps (fn Antiquote.Text t => [token_report SML t] | _ => []))
-      |> tap (List.app check);
+      |> Source.exhaust;
+    val _ = Position.reports (Antiquote.antiq_reports input);
+    val _ =
+      Position.reports_text (maps (fn Antiquote.Text t => [token_report SML t] | _ => []) input);
+    val _ = List.app check input;
   in input @ termination end;
 
 in