Removed QuickAndDirty constructor from simproc_dist datatype.
--- 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 *********************)