src/ZF/Tools/typechk.ML
changeset 36960 01594f816e3a
parent 35409 5c5bb83f2bae
child 38522 de7984a7172b
     1.1 --- a/src/ZF/Tools/typechk.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4      "ZF type-checking";
     1.5  
     1.6  val _ =
     1.7 -  OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
     1.8 +  Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
     1.9      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.10        Toplevel.keep (print_tcset o Toplevel.context_of)));
    1.11