New function name_of_typ.
authorberghofe
Wed Aug 30 13:55:26 2000 +0200 (2000-08-30)
changeset 97401c5b0f27de56
parent 9739 8470c4662685
child 9741 0502f06c2d29
New function name_of_typ.
src/HOL/Tools/datatype_aux.ML
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Aug 30 13:54:57 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Aug 30 13:55:26 2000 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4    type datatype_info
     1.5  
     1.6    exception Datatype
     1.7 +  val name_of_typ : typ -> string
     1.8    val dtyp_of_typ : (string * string list) list -> typ -> dtyp
     1.9    val mk_Free : string -> typ -> int -> term
    1.10    val is_rec_type : dtyp -> bool
    1.11 @@ -198,6 +199,10 @@
    1.12  
    1.13  fun dest_TFree (TFree (n, _)) = n;
    1.14  
    1.15 +fun name_of_typ (Type (s, Ts)) = space_implode "_"
    1.16 +      (filter (not o equal "") (map name_of_typ Ts) @ [Sign.base_name s])
    1.17 +  | name_of_typ _ = "";
    1.18 +
    1.19  fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
    1.20    | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
    1.21    | dtyp_of_typ new_dts (Type (tname, Ts)) =