# HG changeset patch
# User blanchet
# Date 1360919584 -3600
# Node ID 754127b3af235d7d500ce92b16021e78c569e188
# Parent  280ece22765bf49035b61a7bf3e55b820c46fcad
tuned code

diff -r 280ece22765b -r 754127b3af23 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 10:00:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 10:13:04 2013 +0100
@@ -745,30 +745,34 @@
                 Prove (maybe_show outer c [], l, t, by)
             end
           | isar_step_of_direct_inf outer (Cases cases) =
-            let val c = succedent_of_cases cases in
+            let
+              fun do_case (c, infs) =
+                Assume (label_of_clause c, prop_of_clause c) ::
+                map (isar_step_of_direct_inf false) infs
+              val c = succedent_of_cases cases
+              val cases = map do_case cases
+            in
               Prove (maybe_show outer c [Ultimately], label_of_clause c,
-                     prop_of_clause c,
-                     Case_Split (map (do_case false) cases, ([], [])))
+                     prop_of_clause c, Case_Split (cases, ([], [])))
             end
-        and do_case outer (c, infs) =
-          Assume (label_of_clause c, prop_of_clause c) ::
-          map (isar_step_of_direct_inf outer) infs
+        fun isar_proof_of_direct_proof direct_proof =
+          direct_proof
+          |> map (isar_step_of_direct_inf true)
+          |> append assms
         val (isar_proof, (preplay_fail, preplay_time)) =
           refute_graph
           |> redirect_graph axioms tainted bot
-          |> map (isar_step_of_direct_inf true)
-          |> append assms
+          |> isar_proof_of_direct_proof
           |> (if not preplay andalso isar_compress <= 1.0 then
                 rpair (false, (true, seconds 0.0))
               else
                 compress_proof debug ctxt type_enc lam_trans preplay
                   preplay_timeout
                   (if isar_proofs then isar_compress else 1000.0))
-       (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
-          |>> chain_direct_proof
-          |>> kill_useless_labels_in_proof
-          |>> relabel_proof
-          |>> not (null params) ? cons (Fix params)
+          |>> (chain_direct_proof
+               #> kill_useless_labels_in_proof
+               #> relabel_proof
+               #> not (null params) ? cons (Fix params))
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
                            isar_proof