# HG changeset patch
# User berghofe
# Date 967636526 -7200
# Node ID 1c5b0f27de569af9548d17a353dd96929499e39a
# Parent  8470c4662685503ae748d15ead8a8d9ea6352b77
New function name_of_typ.

diff -r 8470c4662685 -r 1c5b0f27de56 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Wed Aug 30 13:54:57 2000 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Wed Aug 30 13:55:26 2000 +0200
@@ -40,6 +40,7 @@
   type datatype_info
 
   exception Datatype
+  val name_of_typ : typ -> string
   val dtyp_of_typ : (string * string list) list -> typ -> dtyp
   val mk_Free : string -> typ -> int -> term
   val is_rec_type : dtyp -> bool
@@ -198,6 +199,10 @@
 
 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])
+  | name_of_typ _ = "";
+
 fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
   | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
   | dtyp_of_typ new_dts (Type (tname, Ts)) =