src/Pure/Syntax/mixfix.ML

   NoSyn |
   Mixfix of string * int list * int |
   Delimfix of string |
   Infixl of int |
   Infixr of int |
-  Binder of string * int * int
+  Binder of string * int * int;
 
 
 (* type / const names *)
 
 fun strip ("'" :: c :: cs) = c :: strip cs

     fun mfix_of (_, _, NoSyn) = []
       | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Mfix (sy, ty, c, ps, p)]
       | 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;
 
     val mfix = flat (map mfix_of const_decls);