name_of_type now replaces non-identifiers by dummy names.
authorberghofe
Wed Nov 13 15:27:27 2002 +0100 (2002-11-13)
changeset 1370755670a70a5f9
parent 13706 9d84cfc77ace
child 13708 a3a410782c95
name_of_type now replaces non-identifiers by dummy names.
src/HOL/Tools/datatype_aux.ML
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Nov 13 15:26:19 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Nov 13 15:27:27 2002 +0100
     1.3 @@ -224,8 +224,11 @@
     1.4  
     1.5  fun dest_TFree (TFree (n, _)) = n;
     1.6  
     1.7 -fun name_of_typ (Type (s, Ts)) = space_implode "_"
     1.8 -      (filter (not o equal "") (map name_of_typ Ts) @ [Sign.base_name s])
     1.9 +fun name_of_typ (Type (s, Ts)) =
    1.10 +      let val s' = Sign.base_name s
    1.11 +      in space_implode "_" (filter (not o equal "") (map name_of_typ Ts) @
    1.12 +        [if Symbol.is_identifier s' then s' else "x"])
    1.13 +      end
    1.14    | name_of_typ _ = "";
    1.15  
    1.16  fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n