--- 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 ^