151 | ((vns,cong)::congs) => ((let |
151 | ((vns,cong)::congs) => ((let |
152 val cert = cterm_of thy |
152 val cert = cterm_of thy |
153 val certy = ctyp_of thy |
153 val certy = ctyp_of thy |
154 val (tyenv, tmenv) = |
154 val (tyenv, tmenv) = |
155 Pattern.match thy |
155 Pattern.match thy |
156 ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) |
156 ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t) |
157 (Envir.type_env (Envir.empty 0), Vartab.empty) |
157 (Vartab.empty, Vartab.empty) |
158 val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) |
158 val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv) |
159 val (fts,its) = |
159 val (fts,its) = |
160 (map (snd o snd) fnvs, |
160 (map (snd o snd) fnvs, |
161 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) |
161 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs) |
162 val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) |
162 val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv) |
202 val certT = ctyp_of thy |
202 val certT = ctyp_of thy |
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 |
207 val (tyenv, tmenv) = Pattern.match thy (rhs_P, t) (Vartab.empty, Vartab.empty) |
208 thy (rhs_P, t) |
|
209 (Envir.type_env (Envir.empty 0), Vartab.empty) |
|
210 val sbst = Envir.subst_vars (tyenv, tmenv) |
208 val sbst = Envir.subst_vars (tyenv, tmenv) |
211 val sbsT = Envir.typ_subst_TVars tyenv |
209 val sbsT = Envir.typ_subst_TVars tyenv |
212 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)) |
213 (Vartab.dest tyenv) |
211 (Vartab.dest tyenv) |
214 val tml = Vartab.dest tmenv |
212 val tml = Vartab.dest tmenv |