# HG changeset patch
# User clasohm
# Date 768652174 -7200
# Node ID 5a7194eeb4ed281a24672596a06b0a4021ac449b
# Parent  e11b893cb7b6e2ddb3fd946545a565eda91665ba
changed implode to ^

diff -r e11b893cb7b6 -r 5a7194eeb4ed src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed May 11 12:14:18 1994 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed May 11 12:29:34 1994 +0200
@@ -268,14 +268,14 @@
 
     fun change_name T ext =
       let val Type (name, ts) = T
-      in Type (implode [name, ext], ts) end;
+      in Type (name ^ ext, ts) end;
 
     (* Append "_H" to lhs if production is not a copy or chain production *)
     fun hide_xprod roots (XProd (lhs, symbs, const, pri)) =
       let fun is_delim (Delim _) = true
             | is_delim _ = false
       in if const <> "" andalso lhs mem roots andalso exists is_delim symbs then
-           XProd (implode [lhs, "_H"], symbs, const, pri)
+           XProd (lhs ^ "_H", symbs, const, pri)
          else XProd (lhs, symbs, const, pri)
       end;