# HG changeset patch
# User steckerm
# Date 1410269581 -7200
# Node ID c723f55747fb6f9d3d798dde03814aed7bd0647a
# Parent  7e54225acef1f929714e1a3f187f80872381a532
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new

diff -r 7e54225acef1 -r c723f55747fb src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Sep 08 23:09:37 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 09 15:33:01 2014 +0200
@@ -383,7 +383,7 @@
                       |> (if waldmeister_new then termify_waldmeister_proof ctxt pool
                           else termify_atp_proof ctxt name format type_enc pool lifted sym_tab)
                       |> spass ? introduce_spass_skolems
-                      |> waldmeister_new ? introduce_waldmeister_skolems (the wm_info)
+                      |> (if waldmeister_new then introduce_waldmeister_skolems (the wm_info) else I)
                       |> factify_atp_proof (map fst used_from) hyp_ts concl_t
                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,