diff -r 1369c27c6966 -r 8e1cde88aae6 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Dec 19 11:48:42 2010 +0100
@@ -246,6 +246,8 @@
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
                    "goal")) [Logic.list_implies (assm_ts, orig_t)]))
+    val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
+                     o Date.fromTimeLocal o Time.now)
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
     val tfree_table =