Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Tue, 09 Sep 2014 17:51:07 +0200
changeset 58248 25af24e1f37b
parent 58246 c723f55747fb (diff)
parent 58247 98d0f85d247f (current diff)
child 58249 180f1b3508ed
merged
--- 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,
isabelle