equal
deleted
inserted
replaced
118 | _ => () |
118 | _ => () |
119 in |
119 in |
120 Conv.all_conv ctrm |
120 Conv.all_conv ctrm |
121 end |
121 end |
122 |
122 |
123 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
124 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
|
125 |
|
126 (* main conversion *) |
123 (* main conversion *) |
127 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
124 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm = |
128 let |
125 let |
129 val first_conv_wrapper = |
126 val first_conv_wrapper = |
130 if trace_enabled ctxt |
127 if trace_enabled ctxt |