changeset 59936 | b8ffc3dc9e24 |
parent 59498 | 50b60f501b05 |
child 60097 | d20ca79d50e4 |
--- a/src/ZF/Tools/typechk.ML Mon Apr 06 16:30:44 2015 +0200 +++ b/src/ZF/Tools/typechk.ML Mon Apr 06 17:06:48 2015 +0200 @@ -126,7 +126,7 @@ "ZF type-checking"); val _ = - Outer_Syntax.command @{command_spec "print_tcset"} "print context of ZF typecheck" + Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck" (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_tcset o Toplevel.context_of)));