# HG changeset patch
# User blanchet
# Date 1626166635 -7200
# Node ID 8d93f9ca6518a48c2bc1ed5f5d090893fcd2fb1e
# Parent  6a0e1c14a8c25cc29ed92888365ac6d65f992cfa
revisited ac28714b7478: more faithful preplaying with chained facts

diff -r 6a0e1c14a8c2 -r 8d93f9ca6518 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 13 10:57:14 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 13 10:57:15 2021 +0200
@@ -70,7 +70,7 @@
      let
        val ctxt = Proof.context_of state
 
-       val fact_names = map fst used_facts
+       val fact_names = used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained) |> map fst
        val {facts = chained, goal, ...} = Proof.goal state
        val goal_t = Logic.get_goal (Thm.prop_of goal) i
 
@@ -93,7 +93,7 @@
                  proof_methods = meths,
                  comment = ""}
            in
-             (case preplay_isar_step ctxt [] timeout [] (mk_step fact_names meths) of
+             (case preplay_isar_step ctxt chained 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
@@ -113,9 +113,7 @@
        try_methss [] methss
      end)
   |> (fn (used_facts, (meth, play)) =>
-        (used_facts |> not (proof_method_distinguishes_chained_and_direct meth)
-           ? filter_out (fn (_, (sc, _)) => sc = Chained),
-         (meth, play)))
+        (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play)))
 
 fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
       expect, induction_rules, ...}) mode writeln_result only learn
@@ -124,7 +122,7 @@
     val ctxt = Proof.context_of state
 
     val hard_timeout = Time.scale 5.0 timeout
-    val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
+    val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length facts |> not only ? Integer.min max_facts
     val induction_rules =
diff -r 6a0e1c14a8c2 -r 8d93f9ca6518 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Jul 13 10:57:14 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Jul 13 10:57:15 2021 +0200
@@ -37,7 +37,6 @@
     ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
   val is_proof_method_direct : proof_method -> bool
-  val proof_method_distinguishes_chained_and_direct : proof_method -> bool
   val string_of_proof_method : string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
@@ -85,9 +84,6 @@
   | is_proof_method_direct Simp_Method = true
   | is_proof_method_direct _ = false
 
-fun proof_method_distinguishes_chained_and_direct Simp_Method = true
-  | proof_method_distinguishes_chained_and_direct _ = false
-
 fun is_proof_method_multi_goal Auto_Method = true
   | is_proof_method_multi_goal _ = false
 
@@ -178,10 +174,7 @@
 fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
   let
     val (indirect_ss, direct_ss) =
-      if is_proof_method_direct meth then
-        ([], extras |> proof_method_distinguishes_chained_and_direct meth ? append used_chaineds)
-      else
-        (extras, [])
+      if is_proof_method_direct meth then ([], extras) else (extras, [])
   in
     (if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^
     apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^