equal
deleted
inserted
replaced
152 |
152 |
153 val mfix = maps mfix_of const_decls; |
153 val mfix = maps mfix_of const_decls; |
154 val xconsts = map #1 const_decls; |
154 val xconsts = map #1 const_decls; |
155 val binders = map_filter binder const_decls; |
155 val binders = map_filter binder const_decls; |
156 val binder_trs = binders |
156 val binder_trs = binders |
157 |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr); |
157 |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr); |
158 val binder_trs' = binders |
158 val binder_trs' = binders |
159 |> map (Syn_Ext.stamp_trfun binder_stamp o |
159 |> map (Syn_Ext.stamp_trfun binder_stamp o |
160 apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap); |
160 apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap); |
161 in |
161 in |
162 Syn_Ext.syn_ext' true is_logtype |
162 Syn_Ext.syn_ext' true is_logtype |
163 mfix xconsts ([], binder_trs, binder_trs', []) ([], []) |
163 mfix xconsts ([], binder_trs, binder_trs', []) ([], []) |
164 end; |
164 end; |
165 |
165 |