diff -r 93c7fcfbe6f5 -r 73372494fd80 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:19:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 11:30:53 2014 +0100
@@ -41,7 +41,7 @@
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
           | minimize_facts mk_step time min_facts (f :: facts) =
-            (case preplay_isar_step 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_facts mk_step time min_facts facts
             | _ => minimize_facts mk_step time (f :: min_facts) facts)
@@ -51,8 +51,7 @@
 
         val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
-        set_preplay_outcomes_of_isar_step ctxt time preplay_data step'
-          [(meth, Lazy.value (Played time))];
+        set_preplay_outcomes_of_isar_step ctxt time preplay_data step' [(meth, Played time)];
         step'
       end
     | _ => step (* don't touch steps that time out or fail *))