changeset 54757 | 4960647932ec |
parent 54756 | dd0f4d265730 |
child 54768 | ee0881a54c72 |
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 15 18:54:26 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 15 19:01:06 2013 +0100 @@ -504,6 +504,7 @@ |> uncombine_term thy |> unlift_term lifted |> infer_formula_types ctxt + |> HOLogic.mk_Trueprop in (name, role, t, rule, deps) end