Exported function make_tnames.
authorberghofe
Wed, 07 Aug 2002 16:43:41 +0200
changeset 13465 08e3fe248ba9
parent 13464 c98321b8d638
child 13466 42766aa25460
Exported function make_tnames.
src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Wed Aug 07 05:54:44 2002 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Wed Aug 07 16:43:41 2002 +0200
@@ -10,6 +10,7 @@
 sig
   val dtK : int ref
   val indexify_names: string list -> string list
+  val make_tnames: typ list -> string list
   val make_injs : (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       term list list