# HG changeset patch
# User blanchet
# Date 1360943619 -3600
# Node ID 58f8716b04ee0298dc970ec68f72d94ddc97b646
# Parent  eba05aaa8612f2f99e075d9d210feadf3b42f43f
tuning

diff -r eba05aaa8612 -r 58f8716b04ee src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 16:40:39 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 16:53:39 2013 +0100
@@ -722,7 +722,8 @@
             end
             |> HOLogic.mk_Trueprop |> close_form
         fun isar_proof_of_direct_proof outer accum [] =
-            rev accum |> outer ? append assms
+            rev accum |> outer ? (append assms
+                                  #> not (null params) ? cons (Fix params))
           | isar_proof_of_direct_proof outer accum (inf :: infs) =
             let
               fun maybe_show outer c =
@@ -779,6 +780,10 @@
                                   Case_Split (map do_case cases)))
                 end
             end
+        val cleanup_labels_in_proof =
+          chain_direct_proof
+          #> kill_useless_labels_in_proof
+          #> relabel_proof
         val (isar_proof, (preplay_fail, preplay_time)) =
           refute_graph
           |> redirect_graph axioms tainted bot
@@ -789,10 +794,7 @@
                 compress_proof debug ctxt type_enc lam_trans preplay
                   preplay_timeout
                   (if isar_proofs then isar_compress else 1000.0))
-          |>> (chain_direct_proof
-               #> kill_useless_labels_in_proof
-               #> relabel_proof
-               #> not (null params) ? cons (Fix params))
+          |>> cleanup_labels_in_proof
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
                            isar_proof