# HG changeset patch
# User nipkow
# Date 1410277867 -7200
# Node ID 25af24e1f37bb5f3f7ae05d04a7e8791c1d770ec
# Parent  c723f55747fb6f9d3d798dde03814aed7bd0647a# Parent  98d0f85d247f0dac82f4157409ebced0bbab84c8
merged

diff -r 98d0f85d247f -r 25af24e1f37b src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 09 17:50:54 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 09 17:51:07 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,