src/Pure/pure_syn.ML

--- a/src/Pure/pure_syn.ML	Tue Mar 25 10:37:10 2014 +0100
+++ b/src/Pure/pure_syn.ML	Tue Mar 25 13:18:10 2014 +0100
@@ -25,7 +25,7 @@
           val source = {delimited = true, text = cat_lines lines, pos = pos};
         in
           gthy
-          |> ML_Context.exec (fn () => ML_Context.eval_source true source)
+          |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
           |> Local_Theory.propagate_ml_env
           |> Context.mapping provide (Local_Theory.background_theory provide)
         end)));