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 {sign, prop, der = (_, prf), ...} = rep_thm thm |
30 let val {thy, prop, der = (_, prf), ...} = rep_thm thm |
31 in Reconstruct.reconstruct_proof sign prop prf end; |
31 in Reconstruct.reconstruct_proof thy prop prf end; |
32 |
32 |
33 fun prf_subst_vars inst = |
33 fun prf_subst_vars inst = |
34 Proofterm.map_proof_terms (subst_vars ([], inst)) I; |
34 Proofterm.map_proof_terms (subst_vars ([], inst)) I; |
35 |
35 |
36 fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT; |
36 fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT; |