src/Pure/Syntax/syntax.ML

 
 fun merge_tokentrtabs tabs1 tabs2 =
   let
     fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
 
+    fun name (s, _) = implode (tl (explode s));
+
     fun merge mode =
       let
         val trs1 = assocs tabs1 mode;
         val trs2 = assocs tabs2 mode;
         val trs = gen_distinct eq_tr (trs1 @ trs2);
       in
         (case gen_duplicates eq_fst trs of
           [] => (mode, trs)
         | dups => error ("More than one token translation function in mode " ^
-            quote mode ^ " for " ^ commas_quote (map fst dups)))
+            quote mode ^ " for " ^ commas_quote (map name dups)))
       end;
   in
     map merge (distinct (map fst (tabs1 @ tabs2)))
   end;