src/Pure/ML/ml_thms.ML

--- a/src/Pure/ML/ml_thms.ML	Thu Mar 27 17:12:40 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Thu Mar 27 17:56:13 2014 +0100
@@ -130,7 +130,7 @@
       else if not (ML_Syntax.is_identifier name) then
         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
       else
-        ML_Compiler.eval {SML = false, verbose = true} Position.none
+        ML_Compiler.eval (ML_Compiler.verbose true ML_Compiler.flags) Position.none
           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
     val _ = Theory.setup (Stored_Thms.put []);
   in () end;