equal
deleted
inserted
replaced
139 val a = Thm.ctyp_of_cterm x; |
139 val a = Thm.ctyp_of_cterm x; |
140 val b = Thm.ctyp_of_cterm t; |
140 val b = Thm.ctyp_of_cterm t; |
141 val ty_insts = map SOME [b, a] |
141 val ty_insts = map SOME [b, a] |
142 val term_insts = map SOME [p, f, x] |
142 val term_insts = map SOME [p, f, x] |
143 in |
143 in |
144 Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} |
144 Thm.instantiate' ty_insts term_insts @{thm eqvt_apply} |
145 end |
145 end |
146 | _ => Conv.no_conv ctrm |
146 | _ => Conv.no_conv ctrm |
147 |
147 |
148 (* conversion for lambdas *) |
148 (* conversion for lambdas *) |
149 fun eqvt_lambda_conv ctrm = |
149 fun eqvt_lambda_conv ctrm = |