--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Tue Feb 04 00:01:54 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Tue Feb 04 00:04:55 2014 +0100
@@ -42,9 +42,7 @@
accum as ([], _) => accum
| accum => collect_subproofs subproofs accum)
in
- (case collect_steps steps (lbls, []) of
- ([], succs) => rev succs
- | _ => raise Fail "Sledgehammer_Isar_Compress: collect_successors")
+ rev (snd (collect_steps steps (lbls, [])))
end
(* traverses steps in reverse post-order and inserts the given updates *)
@@ -75,9 +73,7 @@
(Proof (fix, assms, steps) :: proofs, updates)
end
in
- (case update_steps steps (rev updates) of
- (steps, []) => steps
- | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
+ fst (update_steps steps (rev updates))
end
fun merge_methods preplay_data (l1, meths1) (l2, meths2) =