# HG changeset patch # User wenzelm # Date 1248431563 -7200 # Node ID 541b357299923fc7a46fd1f776b2665351df56e0 # Parent fbada8ed12e60df537c494f870f9e24630dfb179 tuned; diff -r fbada8ed12e6 -r 541b35729992 src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Fri Jul 24 12:00:02 2009 +0200 +++ b/src/ZF/Tools/typechk.ML Fri Jul 24 12:32:43 2009 +0200 @@ -116,7 +116,7 @@ (Method.sections [Args.add -- Args.colon >> K (I, TC_add), Args.del -- Args.colon >> K (I, TC_del)] - >> (K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))) + >> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt)))) "ZF type-checking"; val _ =