equal
deleted
inserted
replaced
263 (* misc rules *) |
263 (* misc rules *) |
264 |
264 |
265 val no_vars = Thm.rule_attribute (fn context => fn th => |
265 val no_vars = Thm.rule_attribute (fn context => fn th => |
266 let |
266 let |
267 val ctxt = Variable.set_body false (Context.proof_of context); |
267 val ctxt = Variable.set_body false (Context.proof_of context); |
268 val ((_, [th']), _) = Variable.import_thms true [th] ctxt; |
268 val ((_, [th']), _) = Variable.import true [th] ctxt; |
269 in th' end); |
269 in th' end); |
270 |
270 |
271 val eta_long = |
271 val eta_long = |
272 Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)); |
272 Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)); |
273 |
273 |