--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100
@@ -17,8 +17,6 @@
val atp_completish : int Config.T
val atp_full_names : bool Config.T
- val is_ho_atp : Proof.context -> string -> bool
-
val run_atp : mode -> string -> prover
end;
@@ -49,16 +47,6 @@
names are enabled by default. *)
val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_names\<close> (K false)
-fun is_atp_of_format is_format ctxt name =
- let val thy = Proof_Context.theory_of ctxt in
- (case try (get_atp thy) name of
- SOME config =>
- exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
- | NONE => false)
- end
-
-val is_ho_atp = is_atp_of_format is_format_higher_order
-
fun choose_type_enc strictness best_type_enc format =
the_default best_type_enc
#> type_enc_of_string strictness