changeset 57460 | 9cc802a8ab06 |
parent 57267 | 8b87114357bd |
child 57671 | dc5e1b1db9ba |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jul 01 16:47:10 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Tue Jul 01 16:47:10 2014 +0200 @@ -383,7 +383,7 @@ val atp_proof = atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab - |> introduce_spass_skolem + |> spass ? introduce_spass_skolem |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,