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