equal
deleted
inserted
replaced
162 | check_args _ NONE = (); |
162 | check_args _ NONE = (); |
163 |
163 |
164 val mfix = map mfix_of type_decls; |
164 val mfix = map mfix_of type_decls; |
165 val _ = map2 check_args type_decls mfix; |
165 val _ = map2 check_args type_decls mfix; |
166 val consts = map (fn (t, _, _) => (t, "")) type_decls; |
166 val consts = map (fn (t, _, _) => (t, "")) type_decls; |
167 in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end; |
167 in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end; |
168 |
168 |
169 |
169 |
170 (* syn_ext_consts *) |
170 (* syn_ext_consts *) |
171 |
171 |
172 val binder_stamp = stamp (); |
172 val binder_stamp = stamp (); |
213 val binder_trs' = binders |
213 val binder_trs' = binders |
214 |> map (Syntax_Ext.stamp_trfun binder_stamp o |
214 |> map (Syntax_Ext.stamp_trfun binder_stamp o |
215 apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap); |
215 apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap); |
216 |
216 |
217 val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls; |
217 val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls; |
218 in |
218 in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end; |
219 Syntax_Ext.syn_ext' logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) |
|
220 end; |
|
221 |
219 |
222 end; |
220 end; |
223 |
221 |
224 structure Basic_Mixfix: BASIC_MIXFIX = Mixfix; |
222 structure Basic_Mixfix: BASIC_MIXFIX = Mixfix; |
225 open Basic_Mixfix; |
223 open Basic_Mixfix; |