src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML

         val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
 
         fun minimize_facts _ time min_facts [] = (time, min_facts)
           | minimize_facts mk_step time min_facts (f :: facts) =
             (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
-              (true, _) => minimize_facts mk_step time (f :: min_facts) facts
-            | (false, time) => minimize_facts mk_step time min_facts facts)
+              Preplay_Success (false, time) => minimize_facts mk_step time min_facts facts
+            | _ => minimize_facts mk_step time (f :: min_facts) facts)
 
         val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
         val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
       in
         set_preplay_result l (Preplay_Success (false, time)); mk_step_lfs_gfs min_lfs min_gfs