src/Pure/ML/ml_thms.ML

--- a/src/Pure/ML/ml_thms.ML	Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Tue Mar 25 13:18:10 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 true Position.none
+        ML_Compiler.eval {SML = false, verbose = true} Position.none
           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
     val _ = Theory.setup (Stored_Thms.put []);
   in () end;