src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -18,6 +18,8 @@
 
 simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}
 
+declare [[simproc del: finite_Collect]]
+
 lemma finite_induct [case_names empty insert, induct set: finite]:
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
   assumes "finite F"