# HG changeset patch
# User blanchet
# Date 1391468695 -3600
# Node ID cddd94fb0e8de8ba26ebe23075c694722285cf7d
# Parent  e7029ee73a97658cb310ffed045b4f2a19b2cef4
tuning

diff -r e7029ee73a97 -r cddd94fb0e8d src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- 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) =