src/HOL/Tools/datatype_prop.ML
changeset 13465 08e3fe248ba9
parent 13340 9b0332344ae2
child 13585 db4005b40cc6
equal deleted inserted replaced
13464:c98321b8d638 13465:08e3fe248ba9
     8 
     8 
     9 signature DATATYPE_PROP =
     9 signature DATATYPE_PROP =
    10 sig
    10 sig
    11   val dtK : int ref
    11   val dtK : int ref
    12   val indexify_names: string list -> string list
    12   val indexify_names: string list -> string list
       
    13   val make_tnames: typ list -> string list
    13   val make_injs : (int * (string * DatatypeAux.dtyp list *
    14   val make_injs : (int * (string * DatatypeAux.dtyp list *
    14     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    15     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    15       term list list
    16       term list list
    16   val make_ind : (int * (string * DatatypeAux.dtyp list *
    17   val make_ind : (int * (string * DatatypeAux.dtyp list *
    17     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
    18     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term