163 (* syn_ext_consts *) |
163 (* syn_ext_consts *) |
164 |
164 |
165 val binder_stamp = stamp (); |
165 val binder_stamp = stamp (); |
166 val binder_name = suffix "_binder"; |
166 val binder_name = suffix "_binder"; |
167 |
167 |
|
168 fun mk_prefix sy = |
|
169 let |
|
170 fun star1 sys = (fst(hd sys) = "*"); |
|
171 val sy' = Input.source_explode (Input.reset_pos sy); |
|
172 val lpar = Symbol_Pos.explode0 ("'(" ^ (if star1 sy' then " " else "")); |
|
173 val rpar = Symbol_Pos.explode0 ((if star1(rev sy') then " " else "") ^ "')") |
|
174 in lpar @ sy' @ rpar end |
|
175 |
168 fun syn_ext_consts logical_types const_decls = |
176 fun syn_ext_consts logical_types const_decls = |
169 let |
177 let |
170 fun mk_infix sy ty c p1 p2 p3 pos = |
178 fun mk_infix sy ty c p1 p2 p3 pos = |
171 [Syntax_Ext.Mfix |
179 [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none), |
172 (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy), |
|
173 ty, c, [], 1000, Position.none), |
|
174 Syntax_Ext.Mfix |
180 Syntax_Ext.Mfix |
175 (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", |
181 (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", |
176 ty, c, [p1, p2], p3, pos)]; |
182 ty, c, [p1, p2], p3, pos)]; |
177 |
183 |
178 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |
184 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |