src/HOL/ex/Cartouche_Examples.thy
changeset 56304 40274e4f5ebf
parent 56278 2576d3a40ed6
child 56499 7e0178c84994
--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Mar 27 17:56:13 2014 +0100
@@ -120,7 +120,7 @@
           ML_Lex.read Position.none "fn _ => (" @
           ML_Lex.read_source false source @
           ML_Lex.read Position.none ");";
-        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
+        val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (#pos source) toks;
       in "" end);
 *}