equal
deleted
inserted
replaced
88 fun mk_mapfun_aux rty = |
88 fun mk_mapfun_aux rty = |
89 case rty of |
89 case rty of |
90 TVar _ => mk_Free rty |
90 TVar _ => mk_Free rty |
91 | Type (_, []) => mk_identity rty |
91 | Type (_, []) => mk_identity rty |
92 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
92 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
93 | _ => raise LIFT_MATCH ("mk_mapfun (default)") |
93 | _ => raise LIFT_MATCH "mk_mapfun (default)" |
94 in |
94 in |
95 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
95 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
96 end |
96 end |
97 |
97 |
98 (* looks up the (varified) rty and qty for |
98 (* looks up the (varified) rty and qty for |
704 (case ty of |
704 (case ty of |
705 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
705 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
706 | x => x) |
706 | x => x) |
707 |
707 |
708 (* subst_trms takes a list of (rtrm, qtrm) substitution pairs |
708 (* subst_trms takes a list of (rtrm, qtrm) substitution pairs |
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 (rtrm, t)) (Vartab.empty, Vartab.empty) of |
714 case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of |