--- a/src/Pure/pure_syn.ML Wed May 07 11:50:30 2014 +0200
+++ b/src/Pure/pure_syn.ML Wed May 07 12:59:15 2014 +0200
@@ -11,9 +11,8 @@
Outer_Syntax.command
(("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
(Thy_Header.args >> (fn header =>
- Toplevel.print o
- Toplevel.init_theory
- (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
+ Toplevel.init_theory
+ (fn () => Thy_Info.toplevel_begin_theory (! ProofGeneral.master_path) header)));
val _ =
Outer_Syntax.command