src/ZF/Tools/typechk.ML

--- a/src/ZF/Tools/typechk.ML	Tue Apr 09 13:55:28 2013 +0200
+++ b/src/ZF/Tools/typechk.ML	Tue Apr 09 15:29:25 2013 +0200
@@ -122,7 +122,7 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+    (Scan.succeed (Toplevel.unknown_context o
       Toplevel.keep (print_tcset o Toplevel.context_of)));