--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100
@@ -868,9 +868,10 @@
let
val problem =
{comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
- subgoal_count = 1, facts = ("", facts), found_proof = K ()}
+ subgoal_count = 1, factss = [("", facts)], found_proof = K ()}
+ val slice = get_default_slice ctxt prover
in
- get_minimizing_prover ctxt MaSh (K ()) prover params problem
+ get_minimizing_prover ctxt MaSh (K ()) prover params problem slice
end
val bad_types = [\<^type_name>\<open>prop\<close>, \<^type_name>\<open>bool\<close>, \<^type_name>\<open>fun\<close>]