equal
deleted
inserted
replaced
102 | strip (c :: cs) = c :: strip cs |
102 | strip (c :: cs) = c :: strip cs |
103 | strip [] = []; |
103 | strip [] = []; |
104 |
104 |
105 val strip_esc = implode o strip o Symbol.explode; |
105 val strip_esc = implode o strip o Symbol.explode; |
106 |
106 |
107 fun deprecated c = (legacy_feature ("unnamed infix operator " ^ quote c); c); |
107 fun deprecated c = (legacy_feature ("Unnamed infix operator " ^ quote c); c); |
108 |
108 |
109 fun type_name t (InfixName _) = t |
109 fun type_name t (InfixName _) = t |
110 | type_name t (InfixlName _) = t |
110 | type_name t (InfixlName _) = t |
111 | type_name t (InfixrName _) = t |
111 | type_name t (InfixrName _) = t |
112 | type_name t (Infix _) = deprecated (strip_esc t) |
112 | type_name t (Infix _) = deprecated (strip_esc t) |