src/Pure/Isar/calculation.ML
changeset 58893 9e0ecb66d6a7
parent 58843 521cea5fa777
child 58950 d07464875dd4
--- a/src/Pure/Isar/calculation.ML	Mon Nov 03 14:31:15 2014 +0100
+++ b/src/Pure/Isar/calculation.ML	Mon Nov 03 14:50:27 2014 +0100
@@ -222,7 +222,7 @@
     (Scan.succeed (Toplevel.proof' ultimately));
 
 val _ =
-  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
+  Outer_Syntax.command @{command_spec "print_trans_rules"} "print transitivity rules"
     (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
 
 end;