1.1 --- a/src/ZF/Tools/typechk.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -118,10 +118,10 @@
     1.4       Args.del -- Args.colon >> K (I, TC_del)]
     1.5    (fn ctxt => Method.SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)));
     1.6  
     1.7 -val _ = OuterSyntax.add_parsers
     1.8 -  [OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
     1.9 +val _ =
    1.10 +  OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
    1.11      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.12 -      Toplevel.keep (print_tcset o Toplevel.context_of)))];
    1.13 +      Toplevel.keep (print_tcset o Toplevel.context_of)));
    1.14  
    1.15  
    1.16  (* theory setup *)