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.
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
authorsteckerm
Tue, 09 Sep 2014 15:33:01 +0200
changeset 58246 c723f55747fb
parent 58245 7e54225acef1
child 58248 25af24e1f37b
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML file | annotate | diff | comparison | revisions 
--- 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,
isabelle