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.
preplay failures might be resolved later, so proceed as usual
authorsmolkas
Fri, 12 Jul 2013 14:18:07 +0200
changeset 52614 3046da935eae
parent 52613 5445f1c53666
child 52615 1e930ee99b0c
preplay failures might be resolved later, so proceed as usual
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Jul 12 14:18:06 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Fri Jul 12 14:18:07 2013 +0200
@@ -138,7 +138,7 @@
         val delta =
           number_of_steps - target_number_of_steps |> Unsynchronized.ref
       in
-        (fn () => not (preplay_fail ()) andalso !delta > 0,
+        (fn () => !delta > 0,
          fn () => delta := !delta - 1)
       end
isabelle