203 val vsns_map = vss ~~ vsns |
203 val vsns_map = vss ~~ vsns |
204 val xns_map = (fst (split_list nths)) ~~ xns |
204 val xns_map = (fst (split_list nths)) ~~ xns |
205 val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map |
205 val subst = map (fn (nt, xn) => (nt, Var ((xn,0), fastype_of nt))) xns_map |
206 val rhs_P = subst_free subst rhs |
206 val rhs_P = subst_free subst rhs |
207 val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty) |
207 val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty) |
208 val sbst = Envir.subst_vars (tyenv, tmenv) |
208 val sbst = Envir.subst_term (tyenv, tmenv) |
209 val sbsT = Envir.typ_subst_TVars tyenv |
209 val sbsT = Envir.subst_type tyenv |
210 val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) |
210 val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t)) |
211 (Vartab.dest tyenv) |
211 (Vartab.dest tyenv) |
212 val tml = Vartab.dest tmenv |
212 val tml = Vartab.dest tmenv |
213 val t's = map (fn xn => snd (the (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) |
213 val t's = map (fn xn => snd (the (AList.lookup (op =) tml (xn,0)))) xns (* FIXME : Express with sbst*) |
214 val (subst_ns, bds) = fold_map |
214 val (subst_ns, bds) = fold_map |