# HG changeset patch # User wenzelm # Date 791210032 -3600 # Node ID 6a054d83acb2628cd393accfd20fd41046485f7b # Parent 9af08725600bad62cf1ddc893a42d9dd97ab3a3a *** empty log message *** diff -r 9af08725600b -r 6a054d83acb2 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;