src/HOL/Tools/datatype_prop.ML
changeset 13465 08e3fe248ba9
parent 13340 9b0332344ae2
child 13585 db4005b40cc6
--- 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