Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
authorblanchet
Mon, 06 Jun 2011 23:26:40 +0200
changeset 43219 371cdc675cf9
parent 43218 d6d084186df0
child 43220 a6bda1a47c0a
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:11:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 23:26:40 2011 +0200
@@ -428,7 +428,7 @@
 fun play_one_line_proof debug timeout ths state i reconstructors =
   let
     fun play [] [] = Failed_to_Play (hd reconstructors)
-      | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
+      | play timed_outs [] = Trust_Playable (List.last timed_outs, SOME timeout)
       | play timed_out (reconstructor :: reconstructors) =
         let val timer = Timer.startRealTimer () in
           case timed_reconstructor reconstructor debug timeout ths state i of
isabelle