diff -r 71eab6907eee -r 600f432ab556 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 10:37:10 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 13:18:10 2014 +0100
@@ -120,7 +120,7 @@
           ML_Lex.read Position.none "fn _ => (" @
           ML_Lex.read_source source @
           ML_Lex.read Position.none ");";
-        val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
+        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
       in "" end);
 *}