equal
deleted
inserted
replaced
692 (* subst_tys takes a list of (rty, qty) substitution pairs |
692 (* subst_tys takes a list of (rty, qty) substitution pairs |
693 and replaces all occurences of rty in the given type |
693 and replaces all occurences of rty in the given type |
694 by appropriate qty, with substitution *) |
694 by appropriate qty, with substitution *) |
695 fun subst_ty thy ty (rty, qty) r = |
695 fun subst_ty thy ty (rty, qty) r = |
696 if r <> NONE then r else |
696 if r <> NONE then r else |
697 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
697 case try (Sign.typ_match thy (rty, ty)) Vartab.empty of |
698 SOME inst => SOME (Envir.subst_type inst qty) |
698 SOME inst => SOME (Envir.subst_type inst qty) |
699 | NONE => NONE |
699 | NONE => NONE |
700 fun subst_tys thy substs ty = |
700 fun subst_tys thy substs ty = |
701 case fold (subst_ty thy ty) substs NONE of |
701 case fold (subst_ty thy ty) substs NONE of |
702 SOME ty => ty |
702 SOME ty => ty |
709 and if the given term matches any of the raw terms it |
709 and if the given term matches any of the raw terms it |
710 returns the appropriate qtrm instantiated. If none of |
710 returns the appropriate qtrm instantiated. If none of |
711 them matched it returns NONE. *) |
711 them matched it returns NONE. *) |
712 fun subst_trm thy t (rtrm, qtrm) s = |
712 fun subst_trm thy t (rtrm, qtrm) s = |
713 if s <> NONE then s else |
713 if s <> NONE then s else |
714 case try (Pattern.match thy (t, rtrm)) (Vartab.empty, Vartab.empty) of |
714 case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of |
715 SOME inst => SOME (Envir.subst_term inst qtrm) |
715 SOME inst => SOME (Envir.subst_term inst qtrm) |
716 | NONE => NONE; |
716 | NONE => NONE; |
717 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
717 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
718 |
718 |
719 (* prepares type and term substitution pairs to be used by above |
719 (* prepares type and term substitution pairs to be used by above |