src/Pure/Thy/thy_output.ML

 
 local
 
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   (fn {context, ...} => fn source =>
-   (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
+   (ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) (ml source);
     Symbol_Pos.source_content source
     |> #1
     |> (if Config.get context quotes then quote else I)
     |> (if Config.get context display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
         else verb_text)));