--- 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) ^ "}" ^