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;