src/HOL/Tools/Datatype/datatype_aux.ML

 
   val app_bnds : term -> int -> term
 
   val indtac : thm -> string list -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
-
-  datatype simproc_dist = FewConstrs of thm list
-                        | ManyConstrs of thm * simpset;
-
 
   exception Datatype
   exception Datatype_Empty of string
   val name_of_typ : typ -> string
   val dtyp_of_typ : (string * string list) list -> typ -> dtyp

       cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
         (Bound 0) params))] exhaustion
   in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   end;
 
-(* handling of distinctness theorems *)
-
-datatype simproc_dist = FewConstrs of thm list
-                      | ManyConstrs of thm * simpset;
 
 (********************** Internal description of datatypes *********************)
 
 datatype dtyp =
     DtTFree of string

   {index : int,
    alt_names : string list option,
    descr : descr,
    sorts : (string * sort) list,
    inject : thm list,
-   distinct : simproc_dist,
+   distinct : thm list,
    induct : thm,
    inducts : thm list,
    exhaust : thm,
    nchotomy : thm,
    rec_names : string list,