src/Pure/Isar/isar_syn.ML
changeset 33515 d066e8369a33
parent 33456 fbd47f9b9b12
child 33553 35f2b30593a8
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 08 13:57:07 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 08 14:38:36 2009 +0100
@@ -780,7 +780,7 @@
 val _ =
   OuterSyntax.improper_command "print_theorems"
       "print theorems of local theory or proof context" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
+    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
 
 val _ =
   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag