*** empty log message ***
authorwenzelm
Fri, 27 Jan 1995 13:33:52 +0100
changeset 887 6a054d83acb2
parent 886 9af08725600b
child 888 3a1de9454d13
*** empty log message ***
src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Jan 27 13:31:26 1995 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Jan 27 13:33:52 1995 +0100
@@ -52,7 +52,7 @@
   Delimfix of string |
   Infixl of int |
   Infixr of int |
-  Binder of string * int * int
+  Binder of string * int * int;
 
 
 (* type / const names *)
@@ -118,8 +118,8 @@
       | 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, p2, p)) =
-          [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p2], p)];
+      | mfix_of (c, ty, Binder (sy, p, q)) =
+          [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)];
 
     fun binder (c, _, Binder (sy, _, _)) = Some (sy, c)
       | binder _ = None;