src/HOL/ex/Cartouche_Examples.thy
changeset 56275 600f432ab556
parent 56072 31e427387ab5
child 56278 2576d3a40ed6
     1.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4            ML_Lex.read Position.none "fn _ => (" @
     1.5            ML_Lex.read_source source @
     1.6            ML_Lex.read Position.none ");";
     1.7 -        val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
     1.8 +        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
     1.9        in "" end);
    1.10  *}
    1.11