equal
deleted
inserted
replaced
712 | NONE => |
712 | NONE => |
713 (case ty of |
713 (case ty of |
714 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
714 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
715 | x => x) |
715 | x => x) |
716 |
716 |
717 fun subst_trm thy t (rt, qt) s = |
717 fun subst_trm thy t (rtrm, qtrm) s = |
718 if s <> NONE then s else |
718 if s <> NONE then s else |
719 case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of |
719 case try (Pattern.match thy (t, rtrm)) (Vartab.empty, Vartab.empty) of |
720 SOME inst => SOME (Envir.subst_term inst qt) |
720 SOME inst => SOME (Envir.subst_term inst qtrm) |
721 | NONE => NONE; |
721 | NONE => NONE; |
722 |
722 |
723 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
723 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
724 |
724 |
725 fun get_ty_trm_substs ctxt = |
725 fun get_ty_trm_substs ctxt = |