src/Pure/Syntax/mixfix.ML

 fun strip ("'" :: c :: cs) = c :: strip cs
   | strip ["'"] = []
   | 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
   | type_name t (Infixl _) = strip_esc t
   | type_name t (Infixr _) = strip_esc t