--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100
@@ -443,12 +443,7 @@
val term_order = AList.lookup (op =) arguments term_orderK
val proof_method_from_msg = proof_method_from_msg arguments
- (* Parse Sledgehammer parameters *)
val params = Sledgehammer_Commands.default_params \<^theory> arguments
- |> (fn (params as {provers, ...}) =>
- (case provers of
- prover :: _ => Sledgehammer_Prover.set_params_provers params [prover]
- | _ => error "sledgehammer action requires one and only one prover"))
val data = Synchronized.var "Mirabelle_Sledgehammer.data" empty_data