diff -r 873b581fd690 -r 30ccc472d486 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -98,7 +98,7 @@
        slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-       factss = [("", facts)], found_proof = I}
+       facts = ("", facts), found_proof = I}
     val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time,
         message} =
       prover params problem