src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     (case AList.lookup (op =) args proverK of
       SOME name => name
     | NONE => default_prover_name ())
   end
 
-fun get_prover ctxt name params goal all_facts =
-  let
-    val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) all_facts
+fun get_prover ctxt name params goal =
+  let
+    val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal)
   in
     Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
   end
 
 type stature = ATP_Problem_Generate.stature

                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
           |> tap (fn factss =>
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^
                      Sledgehammer.string_of_factss factss
                      |> writeln)
-        val prover = get_prover ctxt prover_name params goal facts
+        val prover = get_prover ctxt prover_name params goal
         val problem =
           {comment = "", state = st', goal = goal, subgoal = i,
            subgoal_count = Sledgehammer_Util.subgoal_count st, factss = factss, found_proof = I}
       in prover params problem end)) ()
       handle Timeout.TIMEOUT _ => failed ATP_Proof.TimedOut