author | berghofe |
Wed, 07 Aug 2002 16:43:41 +0200 | |
changeset 13465 | 08e3fe248ba9 |
parent 13464 | c98321b8d638 |
child 13466 | 42766aa25460 |
--- 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