equal
deleted
inserted
replaced
225 val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts); |
225 val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts); |
226 val cenvT = map (apsnd (Thm.ctyp_of sign)) envT; |
226 val cenvT = map (apsnd (Thm.ctyp_of sign)) envT; |
227 val cenv = |
227 val cenv = |
228 map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) |
228 map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) |
229 (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts)); |
229 (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts)); |
230 in Thm.instantiate (cenvT, cenv) thm end; |
230 in Drule.instantiate (cenvT, cenv) thm end; |
231 |
231 |
232 fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x; |
232 fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x; |
233 |
233 |
234 fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of)); |
234 fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of)); |
235 |
235 |