# HG changeset patch
# User berghofe
# Date 1207237850 -7200
# Node ID 3fc9730403c1382fa6a187f99e5a49fc4e13cf5f
# Parent  96e82c7861faaefe1c4eb20bf660f941888dfe75
Removed QuickAndDirty constructor from simproc_dist datatype.

diff -r 96e82c7861fa -r 3fc9730403c1 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Thu Apr 03 17:49:39 2008 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Thu Apr 03 17:50:50 2008 +0200
@@ -30,8 +30,7 @@
   val indtac : thm -> string list -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
 
-  datatype simproc_dist = QuickAndDirty
-                        | FewConstrs of thm list
+  datatype simproc_dist = FewConstrs of thm list
                         | ManyConstrs of thm * simpset;
 
   datatype dtyp =
@@ -164,8 +163,7 @@
 
 (* handling of distinctness theorems *)
 
-datatype simproc_dist = QuickAndDirty
-                      | FewConstrs of thm list
+datatype simproc_dist = FewConstrs of thm list
                       | ManyConstrs of thm * simpset;
 
 (********************** Internal description of datatypes *********************)