Removed QuickAndDirty constructor from simproc_dist datatype.
authorberghofe
Thu Apr 03 17:50:50 2008 +0200 (2008-04-03)
changeset 265323fc9730403c1
parent 26531 96e82c7861fa
child 26533 aeef55a3d1d5
Removed QuickAndDirty constructor from simproc_dist datatype.
src/HOL/Tools/datatype_aux.ML
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Apr 03 17:49:39 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Apr 03 17:50:50 2008 +0200
     1.3 @@ -30,8 +30,7 @@
     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 = QuickAndDirty
     1.8 -                        | FewConstrs of thm list
     1.9 +  datatype simproc_dist = FewConstrs of thm list
    1.10                          | ManyConstrs of thm * simpset;
    1.11  
    1.12    datatype dtyp =
    1.13 @@ -164,8 +163,7 @@
    1.14  
    1.15  (* handling of distinctness theorems *)
    1.16  
    1.17 -datatype simproc_dist = QuickAndDirty
    1.18 -                      | FewConstrs of thm list
    1.19 +datatype simproc_dist = FewConstrs of thm list
    1.20                        | ManyConstrs of thm * simpset;
    1.21  
    1.22  (********************** Internal description of datatypes *********************)