equal
deleted
inserted
replaced
72 in |
72 in |
73 if null dups then () else error (message ^ commas dups) |
73 if null dups then () else error (message ^ commas dups) |
74 end; |
74 end; |
75 |
75 |
76 fun match_bind (n, b) = (n = Binding.base_name b); |
76 fun match_bind (n, b) = (n = Binding.base_name b); |
77 fun parm_eq ((b1, mx1), (b2, mx2)) = |
77 fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) = |
78 (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *) |
78 (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *) |
79 (Binding.base_name b1 = Binding.base_name b2) andalso |
79 (Binding.base_name b1 = Binding.base_name b2) andalso |
80 (if mx1 = mx2 then true |
80 (if mx1 = mx2 then true |
81 else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^ |
81 else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^ |
82 " in expression.")); |
82 " in expression.")); |