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.
avoid passing chained facts twice to preplay in Sledgehammer
authorblanchet
Thu, 23 Apr 2020 16:52:14 +0200
changeset 71794 ac28714b7478
parent 71793 e771b8157fc7
child 71797 54d4bfa48025
avoid passing chained facts twice to preplay in Sledgehammer
src/HOL/Tools/Sledgehammer/sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Apr 23 15:45:42 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Apr 23 16:52:14 2020 +0200
@@ -85,7 +85,7 @@
              fun mk_step fact_names meths =
                Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
            in
-             (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
+             (case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of
                (res as (meth, Played time)) :: _ =>
                (* if a fact is needed by an ATP, it will be needed by "metis" *)
                if not minimize orelse is_metis_method meth then
isabelle