--- 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 =