| changeset 4697 | 101d384b69b2 |
| parent 4143 | 4bd5f4c05cf6 |
| child 4823 | 588538fb9308 |
--- a/src/Pure/Syntax/mixfix.ML Mon Mar 09 16:10:22 1998 +0100 +++ b/src/Pure/Syntax/mixfix.ML Mon Mar 09 16:10:38 1998 +0100 @@ -68,7 +68,7 @@ | strip (c :: cs) = c :: strip cs | strip [] = []; -val strip_esc = implode o strip o explode; +val strip_esc = implode o strip o Symbol.explode; fun type_name t (InfixlName _) = t | type_name t (InfixrName _) = t