src/ZF/Tools/typechk.ML
changeset 36960 01594f816e3a
parent 35409 5c5bb83f2bae
child 38522 de7984a7172b
--- a/src/ZF/Tools/typechk.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/ZF/Tools/typechk.ML	Mon May 17 23:54:15 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)));