--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Sun Feb 02 20:53:51 2014 +0100
@@ -51,43 +51,40 @@
fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
let
- val add_lfs = fold (Ord_List.insert label_ord)
-
- fun do_proof (Proof (fix, assms, steps)) =
- let val (refed, steps) = do_steps steps in
+ fun process_proof (Proof (fix, assms, steps)) =
+ let val (refed, steps) = process_steps steps in
(refed, Proof (fix, assms, steps))
end
- and do_steps [] = ([], [])
- | do_steps steps =
+ and process_steps [] = ([], [])
+ | process_steps steps =
(* the last step is always implicitly referenced *)
- let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in
- fold_rev do_step steps (refed, [concl])
+ let val (steps, (refed, concl)) = split_last steps ||> process_referenced_step in
+ fold_rev process_step steps (refed, [concl])
end
- and do_step step (refed, accu) =
+ and process_step step (refed, accu) =
(case label_of_isar_step step of
NONE => (refed, step :: accu)
| SOME l =>
if Ord_List.member label_ord refed l then
- do_refed_step step
+ process_referenced_step step
|>> Ord_List.union label_ord refed
||> (fn x => x :: accu)
else
(refed, accu))
- and do_refed_step step = step |> postproc_step |> do_refed_step'
- and do_refed_step' (Let _) = raise Fail "Sledgehammer_Isar_Minimize"
- | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
- let
- val (refed, subproofs) =
- map do_proof subproofs
- |> split_list
- |>> Ord_List.unions label_ord
- |>> add_lfs lfs
- val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
- in
- (refed, step)
- end
+ and process_referenced_step step = step |> postproc_step |> process_referenced_step_subproofs
+ and process_referenced_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
+ let
+ val (refed, 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), m))
+ in
+ (refed, step)
+ end
in
- snd o do_proof
+ snd o process_proof
end
end;