# HG changeset patch
# User wenzelm
# Date 1621588793 -7200
# Node ID f4be1b0d7a5189a0b33bd0c4d070c5728f7d33b3
# Parent  74078d50d77b356479d2106455b41c50e4fc21ab
tuned;

diff -r 74078d50d77b -r f4be1b0d7a51 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Fri May 21 10:15:38 2021 +0200
+++ b/src/Doc/antiquote_setup.ML	Fri May 21 11:19:53 2021 +0200
@@ -77,8 +77,8 @@
   (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
   (fn ctxt => fn (source1, opt_source2) =>
     let
-      val (txt1, toks1) = prep_ml source1;
-      val (txt2, toks2) =
+      val (txt1, ants1) = prep_ml source1;
+      val (txt2, ants2) =
         (case opt_source2 of
           SOME source => prep_ml source
         | NONE => ("", []));
@@ -94,7 +94,7 @@
 
       val pos = Input.pos_of source1;
       val _ =
-        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
+        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (ants1, ants2))
           handle ERROR msg => error (msg ^ Position.here pos);
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in