--- a/src/Pure/Syntax/mixfix.ML Wed Jan 18 10:17:55 1995 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Jan 18 11:36:04 1995 +0100
@@ -13,7 +13,7 @@
Delimfix of string |
Infixl of int |
Infixr of int |
- Binder of string * int
+ Binder of string * int * int
val max_pri: int
end;
@@ -52,7 +52,7 @@
Delimfix of string |
Infixl of int |
Infixr of int |
- Binder of string * int;
+ Binder of string * int * int
(* type / const names *)
@@ -118,10 +118,10 @@
| mfix_of (c, ty, Delimfix sy) = [Mfix (sy, ty, c, [], max_pri)]
| mfix_of (sy, ty, Infixl p) = mk_infix sy ty (infix_name sy) p (p + 1) p
| mfix_of (sy, ty, Infixr p) = mk_infix sy ty (infix_name sy) (p + 1) p p
- | mfix_of (c, ty, Binder (sy, p)) =
- [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [], p)];
+ | mfix_of (c, ty, Binder (sy, p2, p)) =
+ [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p2], p)];
- fun binder (c, _, Binder (sy, _)) = Some (sy, c)
+ fun binder (c, _, Binder (sy, _, _)) = Some (sy, c)
| binder _ = None;
val mfix = flat (map mfix_of const_decls);