# HG changeset patch
# User blanchet
# Date 1587653534 -7200
# Node ID ac28714b74782108e1cd241dc57644b110c3ee70
# Parent  e771b8157fc74c15dd1fda4b87a25d47acde9019
avoid passing chained facts twice to preplay in Sledgehammer

diff -r e771b8157fc7 -r ac28714b7478 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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