diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sat Mar 01 22:46:31 2014 +0100
@@ -86,7 +86,9 @@
         then txt1 ^ ": " ^ txt2
         else txt1 ^ " : " ^ txt2;
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
-      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
+      val _ =  (* ML_Lex.read (!?) *)
+        ML_Context.eval_source_in (SOME ctxt) false
+          {delimited = false, text = ml (txt1, txt2), pos = Position.none};
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^