diff -r 6f77310a0907 -r b18f65f77fcd src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -25,8 +25,9 @@
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
 
-fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, _)) =
-    Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l])
+fun keep_fastest_method_of_isar_step preplay_data (Prove (qs, xs, l, t, subproofs, facts, meths)) =
+    Prove (qs, xs, l, t, subproofs, facts,
+      meths |> List.partition (curry (op =) (fastest_method_of_isar_step preplay_data l)) |> op @)
   | keep_fastest_method_of_isar_step _ step = step
 
 val slack = seconds 0.1