src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32900 dc883c6126d4
parent 32733 71618deaf777
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Oct 09 13:34:34 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Oct 09 13:34:40 2009 +0200
     1.3 @@ -38,10 +38,6 @@
     1.4    val indtac : thm -> string list -> int -> tactic
     1.5    val exh_tac : (string -> thm) -> int -> tactic
     1.6  
     1.7 -  datatype simproc_dist = FewConstrs of thm list
     1.8 -                        | ManyConstrs of thm * simpset;
     1.9 -
    1.10 -
    1.11    exception Datatype
    1.12    exception Datatype_Empty of string
    1.13    val name_of_typ : typ -> string
    1.14 @@ -153,10 +149,6 @@
    1.15    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    1.16    end;
    1.17  
    1.18 -(* handling of distinctness theorems *)
    1.19 -
    1.20 -datatype simproc_dist = FewConstrs of thm list
    1.21 -                      | ManyConstrs of thm * simpset;
    1.22  
    1.23  (********************** Internal description of datatypes *********************)
    1.24  
    1.25 @@ -176,7 +168,7 @@
    1.26     descr : descr,
    1.27     sorts : (string * sort) list,
    1.28     inject : thm list,
    1.29 -   distinct : simproc_dist,
    1.30 +   distinct : thm list,
    1.31     induct : thm,
    1.32     inducts : thm list,
    1.33     exhaust : thm,