src/Pure/Syntax/syntax.ML
changeset 2706 91a640a91c6e
parent 2700 80e6b48c5204
child 2913 ce271fa4d8e2
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Feb 28 16:58:42 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Feb 28 21:54:37 1997 +0100
     1.3 @@ -106,6 +106,8 @@
     1.4    let
     1.5      fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2;
     1.6  
     1.7 +    fun name (s, _) = implode (tl (explode s));
     1.8 +
     1.9      fun merge mode =
    1.10        let
    1.11          val trs1 = assocs tabs1 mode;
    1.12 @@ -115,7 +117,7 @@
    1.13          (case gen_duplicates eq_fst trs of
    1.14            [] => (mode, trs)
    1.15          | dups => error ("More than one token translation function in mode " ^
    1.16 -            quote mode ^ " for " ^ commas_quote (map fst dups)))
    1.17 +            quote mode ^ " for " ^ commas_quote (map name dups)))
    1.18        end;
    1.19    in
    1.20      map merge (distinct (map fst (tabs1 @ tabs2)))