diff -r dc542b78ef0f -r c3b5cb53ea79 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Tue Jul 01 17:16:11 2014 +0200 +++ b/src/Doc/antiquote_setup.ML Tue Jul 01 17:59:56 2014 +0200 @@ -99,8 +99,10 @@ else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; + val pos = #pos source1; val _ = - ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2)); + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) + handle ERROR msg => error (msg ^ Position.here pos); val kind' = if kind = "" then "ML" else "ML " ^ kind; in "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^