equal
deleted
inserted
replaced
150 [Drule.generalize (Names.empty, Names.make_set [#1 (dest_Free v)]) eq]) |
150 [Drule.generalize (Names.empty, Names.make_set [#1 (dest_Free v)]) eq]) |
151 |> Drule.zero_var_indexes |
151 |> Drule.zero_var_indexes |
152 end |
152 end |
153 |
153 |
154 (* Destruct the abstraction and apply the conversion. *) |
154 (* Destruct the abstraction and apply the conversion. *) |
155 val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt |
155 val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt |
156 val (v, ct') = Thm.dest_abs_name u ct |
|
157 val eq = cv (v, ctxt') ct' |
156 val eq = cv (v, ctxt') ct' |
158 in |
157 in |
159 if Thm.is_reflexive eq |
158 if Thm.is_reflexive eq |
160 then all_cconv ct |
159 then all_cconv ct |
161 else abstract_rule (Thm.term_of v) eq |
160 else abstract_rule (Thm.term_of v) eq |