# HG changeset patch
# User blanchet
# Date 1391452322 -3600
# Node ID b18f65f77fcdd906409bc591031c8d4b76fafb0a
# Parent  6f77310a0907f2002b3ca8ec935546f467b5f166
keep all proof methods in data structure until the end, to enhance debugging output

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
diff -r 6f77310a0907 -r b18f65f77fcd src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -208,7 +208,7 @@
   #> fst
 
 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
-    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
+    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime
 
 fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =