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); *}