diff -r 40d565e51dea -r 68400ea32f7b src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri May 13 13:56:22 1994 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Tue May 17 14:42:34 1994 +0200
@@ -268,14 +268,14 @@
 
     fun change_name T ext =
       let val Type (name, ts) = T
-      in Type (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 (lhs ^ "_H", symbs, const, pri)
+           XProd ("@" ^ lhs ^ "_H", symbs, const, pri)
          else XProd (lhs, symbs, const, pri)
       end;