# HG changeset patch
# User berghofe
# Date 1028731421 -7200
# Node ID 08e3fe248ba9c2c3c5c98226625d4f828c7b0660
# Parent  c98321b8d63832e2ca1c355afc82405829c98932
Exported function make_tnames.

diff -r c98321b8d638 -r 08e3fe248ba9 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