308 fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % SOME x % SOME y %% |
308 fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % SOME x % SOME y %% |
309 prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1 |
309 prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1 |
310 | strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps) |
310 | strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps) |
311 | strip_cong _ _ = NONE; |
311 | strip_cong _ _ = NONE; |
312 |
312 |
313 val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst)))); |
313 val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of @{thm subst})))); |
314 val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym)))); |
314 val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of@{thm sym})))); |
315 |
315 |
316 fun make_subst Ts prf xs (_, []) = prf |
316 fun make_subst Ts prf xs (_, []) = prf |
317 | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) = |
317 | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) = |
318 let val T = fastype_of1 (Ts, x) |
318 let val T = fastype_of1 (Ts, x) |
319 in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps) |
319 in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps) |