equal
deleted
inserted
replaced
25 fun forall_intr_prf (t, prf) = |
25 fun forall_intr_prf (t, prf) = |
26 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
26 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) |
27 in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; |
27 in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; |
28 |
28 |
29 fun prf_of thm = |
29 fun prf_of thm = |
30 let val {thy, prop, der = (_, prf), ...} = rep_thm thm |
30 Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); |
31 in Reconstruct.reconstruct_proof thy prop prf end; |
|
32 |
31 |
33 fun prf_subst_vars inst = |
32 fun prf_subst_vars inst = |
34 Proofterm.map_proof_terms (subst_vars ([], inst)) I; |
33 Proofterm.map_proof_terms (subst_vars ([], inst)) I; |
35 |
34 |
36 fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT; |
35 fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT; |