author | wenzelm |
Mon, 09 Mar 1998 16:10:38 +0100 | |
changeset 4697 | 101d384b69b2 |
parent 4696 | ff89fc67cc7a |
child 4698 | 44e33cfdbb46 |
--- 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