1signature ConsThms =
2sig
3  type thm = Thm.thm
4
5  val build : {New_Ty_Existence_Thm : thm,
6               New_Ty_Induct_Thm : thm,
7               New_Ty_Uniqueness_Thm : thm}
8              ->
9                 {mutual_constructors_distinct : thm,
10                  mutual_constructors_one_one : thm,
11                  mutual_cases : thm,
12                  argument_extraction_definitions : (string * thm) list}
13
14end
15