src/Pure/Isar/isar_syn.ML
changeset 24871 6af56e53734a
parent 24868 2990c327d8c6
child 24914 95cda5dd58d5
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Oct 06 17:46:49 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 06 17:46:51 2007 +0200
     1.3 @@ -742,11 +742,11 @@
     1.4  
     1.5  val _ =
     1.6    OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
     1.7 -    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
     1.8 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
    1.12 -    (Scan.succeed (Toplevel.no_timing o OuterSyntax.print_commands));
    1.13 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
    1.14  
    1.15  val _ =
    1.16    OuterSyntax.improper_command "print_configs" "print configuration options" K.diag