--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 11:37:48 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 03 11:58:38 2014 +0100
@@ -25,19 +25,18 @@
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, _)) =
+ Prove (qs, xs, l, t, subproofs, facts, [fastest_method_of_isar_step preplay_data l])
| keep_fastest_method_of_isar_step _ step = step
val slack = seconds 0.1
fun minimize_isar_step_dependencies ctxt preplay_data
- (step as Prove (qs, xs, l, t, subproofs, ((lfs0, gfs0), meths as meth :: _))) =
+ (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _)) =
(case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
Played time =>
let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)
fun minimize_facts _ time min_facts [] = (time, min_facts)
| minimize_facts mk_step time min_facts (f :: facts) =
@@ -76,16 +75,15 @@
else
(used, accu))
and process_used_step step = step |> postproc_step |> process_used_step_subproofs
- and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
+ and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths)) =
let
val (used, subproofs) =
map process_proof subproofs
|> split_list
|>> Ord_List.unions label_ord
|>> fold (Ord_List.insert label_ord) lfs
- val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
in
- (used, step)
+ (used, Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths))
end
in
snd o process_proof