--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 10:01:50 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100
@@ -94,8 +94,8 @@
induction_rules = induction_rules, max_facts = SOME (length facts),
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = false,
- minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
+ compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize,
+ 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}