diff -r bfe7573a239b -r e3c4e337196c src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 10:58:50 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 04 13:57:56 2009 +0200
@@ -55,7 +55,7 @@
       TimeLimit.timeLimit timeout atp (Proof.get_goal st)
   in if success then (message, SOME (time, thm_names)) else (message, NONE) end
   handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
-       | TimeLimit.TimeOut => ("time out", NONE)
+       | TimeLimit.TimeOut => ("timeout", NONE)
        | ERROR msg => ("error: " ^ msg, NONE)
 
 in
@@ -87,7 +87,7 @@
     fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
     fun timed_metis thms =
       uncurry with_time (Mirabelle.cpu_time apply_metis thms)
-      handle TimeLimit.TimeOut => "time out"
+      handle TimeLimit.TimeOut => "timeout"
            | ERROR msg => "error: " ^ msg
     fun log_metis s = log (metis_tag ^ s)
   in