# HG changeset patch
# User wenzelm
# Date 889456238 -3600
# Node ID 101d384b69b2fb9a82a68983dca03e45a078c170
# Parent  ff89fc67cc7a66c8e1b24dde9c5777583cc58990
Symbol.explode;

diff -r ff89fc67cc7a -r 101d384b69b2 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