src/Pure/Thy/thy_output.ML
changeset 56275 600f432ab556
parent 56204 f70e69208a8c
child 56278 2576d3a40ed6
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -639,7 +639,7 @@
     1.4  
     1.5  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
     1.6    (fn {context, ...} => fn source =>
     1.7 -   (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
     1.8 +   (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
     1.9      Symbol_Pos.source_content source
    1.10      |> #1
    1.11      |> (if Config.get context quotes then quote else I)