# HG changeset patch
# User wenzelm
# Date 1361548330 -3600
# Node ID 83252b0605be8810080b9bd6a83a0ef5bf65964b
# Parent  a7a04b449e8bcc48d9b0f68c5c25b2dcc9d5dcd3
make SML/NJ happy;

diff -r a7a04b449e8b -r 83252b0605be src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Feb 22 14:39:12 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Feb 22 16:52:10 2013 +0100
@@ -633,7 +633,7 @@
 
 local
 
-fun timing_message tr t =
+fun timing_message tr (t: Timing.timing) =
   if Timing.is_relevant_time (#elapsed t) andalso not (Position.is_reported (pos_of tr))
   then
     (case approximative_id tr of