Symbol.explode;
authorwenzelm
Mon, 09 Mar 1998 16:10:38 +0100
changeset 4697 101d384b69b2
parent 4696 ff89fc67cc7a
child 4698 44e33cfdbb46
Symbol.explode;
src/Pure/Syntax/mixfix.ML
--- 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