# HG changeset patch
# User wenzelm
# Date 1191685611 -7200
# Node ID 6af56e53734a17850829df9e74f2b2fa8e5c2005
# Parent  9d057ff8e74c14e2d241b86ba86e0c620a885bc5
tuned;

diff -r 9d057ff8e74c -r 6af56e53734a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Oct 06 17:46:49 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 06 17:46:51 2007 +0200
@@ -742,11 +742,11 @@
 
 val _ =
   OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
-    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
 
 val _ =
   OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
-    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
 
 val _ =
   OuterSyntax.improper_command "print_configs" "print configuration options" K.diag