--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:22:31 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Thu Dec 19 18:39:54 2013 +0100
@@ -36,8 +36,8 @@
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