equal
deleted
inserted
replaced
69 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
69 | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) |
70 in |
70 in |
71 Conv.no_conv ctrm |
71 Conv.no_conv ctrm |
72 end |
72 end |
73 |
73 |
74 |
|
75 (* conversion for applications: |
74 (* conversion for applications: |
76 only applies the conversion, if the head of the |
75 only applies the conversion, if the head of the |
77 application is not a "bad head" *) |
76 application is not a "bad head" *) |
78 fun has_bad_head bad_hds trm = |
77 fun has_bad_head bad_hds trm = |
79 case (head_of trm) of |
78 case (head_of trm) of |
130 val first_conv_wrapper = |
129 val first_conv_wrapper = |
131 if trace_enabled ctxt |
130 if trace_enabled ctxt |
132 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
131 then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) |
133 else Conv.first_conv |
132 else Conv.first_conv |
134 |
133 |
135 val pre_thms = (map safe_mk_equiv user_thms) @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt) |
134 val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt |
136 val post_thms = @{thms permute_pure[THEN eq_reflection]} |
135 val post_thms = map safe_mk_equiv @{thms permute_pure} |
137 in |
136 in |
138 first_conv_wrapper |
137 first_conv_wrapper |
139 [ More_Conv.rewrs_conv pre_thms, |
138 [ More_Conv.rewrs_conv pre_thms, |
140 eqvt_apply_conv bad_hds, |
139 eqvt_apply_conv bad_hds, |
141 eqvt_lambda_conv, |
140 eqvt_lambda_conv, |