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/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 54823 a510fc40559c
parent 54816 10d48c2a3e32
child 54824 4e58a38b330b 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 17:24:17 2013 +0100
@@ -405,7 +405,8 @@
 fun isar_proof_would_be_a_good_idea preplay =
   (case preplay of
     Played (reconstr, _) => reconstr = SMT
-  | Play_Timed_Out _ => false
+  | Not_Played _ => false
+  | Play_Timed_Out _ => true
   | Play_Failed _ => true)
 
 fun proof_text ctxt isar_proofs isar_params num_chained
isabelle