| changeset 36972 | aa4bc5a4be1d |
| parent 36960 | 01594f816e3a |
| child 38522 | de7984a7172b |
--- a/src/ZF/Tools/typechk.ML Mon May 17 12:00:10 2010 -0700 +++ b/src/ZF/Tools/typechk.ML Tue May 18 00:01:51 2010 +0200 @@ -118,7 +118,7 @@ "ZF type-checking"; val _ = - OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag + Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o Toplevel.keep (print_tcset o Toplevel.context_of)));