# HG changeset patch
# User berghofe
# Date 1037197647 -3600
# Node ID 55670a70a5f921e95f3b80afb9d06ce83ec7a281
# Parent  9d84cfc77aceb89eac94d1d04aa03fed4a0652ca
name_of_type now replaces non-identifiers by dummy names.

diff -r 9d84cfc77ace -r 55670a70a5f9 src/HOL/Tools/datatype_aux.ML
--- 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