src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

                    Library.foldr1 s_disj pos)
               | _ => fold (curry s_disj) lits @{term False}
             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 =
                 (outer andalso length c = 1 andalso subset (op =) (c, conjs))
                 ? cons Show

                   do_rest (Prove (maybe_show outer c [Ultimately],
                                   label_of_clause c, prop_of_clause c,
                                   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
           |> isar_proof_of_direct_proof true []
           |> (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))
-          |>> (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
       in
         case isar_text of