114 fun syn_ext_consts logtypes const_decls = |
114 fun syn_ext_consts logtypes const_decls = |
115 let |
115 let |
116 fun name_of (c, _, mx) = const_name c mx; |
116 fun name_of (c, _, mx) = const_name c mx; |
117 |
117 |
118 fun mk_infix sy ty c p1 p2 p3 = |
118 fun mk_infix sy ty c p1 p2 p3 = |
119 [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3), |
119 [Mfix ("op " ^ sy, ty, c, [], max_pri), |
120 Mfix ("op " ^ sy, ty, c, [], max_pri)]; |
120 Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; |
121 |
121 |
122 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |
122 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |
123 [Type ("idts", []), ty2] ---> ty3 |
123 [Type ("idts", []), ty2] ---> ty3 |
124 | binder_typ c _ = error ("Bad type of binder " ^ quote c); |
124 | binder_typ c _ = error ("Bad type of binder " ^ quote c); |
125 |
125 |