--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 01 18:45:18 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 01 19:57:58 2016 +0100
@@ -45,7 +45,7 @@
fun minimize_half _ min_facts [] time = (min_facts, time)
| minimize_half mk_step min_facts (fact :: facts) time =
- (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
+ (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth
(mk_step (min_facts @ facts)) of
Played time' => minimize_half mk_step min_facts facts time'
| _ => minimize_half mk_step (fact :: min_facts) facts time)