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_run.ML
changeset 43292 ff3d49e77359
parent 43290 07eb0ad9bb93
child 43306 03e6da81aee6 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 16:20:18 2011 +0200
@@ -77,7 +77,7 @@
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
              (result as {outcome, used_facts, run_time_in_msecs, preplay,
                          message, message_tail} : prover_result) =
-  if is_some outcome then
+  if is_some outcome orelse null used_facts then
     result
   else
     let
isabelle