tuned;
authorwenzelm
Sat, 06 Oct 2007 17:46:51 +0200
changeset 24871 6af56e53734a
parent 24870 9d057ff8e74c
child 24872 7fd1aa6671a4
tuned;
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