# HG changeset patch
# User desharna
# Date 1743441471 -7200
# Node ID 667c67b1e8f1fbca7e84373a7c1d04430ea51788
# Parent  381970dd5b21e93680f8eae54a907d533acdfa12
tuned

diff -r 381970dd5b21 -r 667c67b1e8f1 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Mar 31 18:58:24 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Mar 31 19:17:51 2025 +0200
@@ -220,7 +220,7 @@
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command meth i n used_chaineds extras =
+fun proof_method_command meth i n extras =
   let
     val (indirect_facts, direct_facts) =
       if is_proof_method_direct meth then ([], extras) else (extras, [])
@@ -247,9 +247,9 @@
     Markup.markup (Markup.break {width = 1, indent = 2}) " ")
 
 fun one_line_proof_text ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
-  let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
+  let val extra = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts in
     map fst extra
-    |> proof_method_command meth subgoal subgoal_count (map fst chained)
+    |> proof_method_command meth subgoal subgoal_count
     |> (if play = Play_Failed then failed_command_line else try_command_line banner play)
   end