# HG changeset patch
# User blanchet
# Date 1360942839 -3600
# Node ID eba05aaa8612f2f99e075d9d210feadf3b42f43f
# Parent  4e53be4ad84536dc1a6c6b9038b29672dc757288
repaired collateral damage from 4f0147ed8bcb

diff -r 4e53be4ad845 -r eba05aaa8612 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 16:17:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Feb 15 16:40:39 2013 +0100
@@ -721,7 +721,8 @@
               | _ => fold (curry s_disj) lits @{term False}
             end
             |> HOLogic.mk_Trueprop |> close_form
-        fun isar_proof_of_direct_proof _ accum [] = assms @ rev accum
+        fun isar_proof_of_direct_proof outer accum [] =
+            rev accum |> outer ? append assms
           | isar_proof_of_direct_proof outer accum (inf :: infs) =
             let
               fun maybe_show outer c =