Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 32518 e3c4e337196c
parent 32515 e7c0d3c0494a
child 32521 f20cc66b2c74 
--- 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
isabelle