name_of_type now replaces non-identifiers by dummy names.

--- a/src/HOL/Tools/datatype_aux.ML	Wed Nov 13 15:26:19 2002 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Wed Nov 13 15:27:27 2002 +0100
@@ -224,8 +224,11 @@
 
 fun dest_TFree (TFree (n, _)) = n;
 
-fun name_of_typ (Type (s, Ts)) = space_implode "_"
-      (filter (not o equal "") (map name_of_typ Ts) @ [Sign.base_name s])
+fun name_of_typ (Type (s, Ts)) =
+      let val s' = Sign.base_name s
+      in space_implode "_" (filter (not o equal "") (map name_of_typ Ts) @
+        [if Symbol.is_identifier s' then s' else "x"])
+      end
   | name_of_typ _ = "";
 
 fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n