src/HOL/Finite_Set.thy

 inductive finite :: "'a set \<Rightarrow> bool"
   where
     emptyI [simp, intro!]: "finite {}"
   | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
 
+(* FIXME: move to Set theory *)
 use "Tools/set_comprehension_pointfree.ML"
 
 simproc_setup finite_Collect ("finite (Collect P)") =
   {* Set_Comprehension_Pointfree.simproc *}
 
+(* FIXME: move to Set theory*)
+setup {*
+  Code_Preproc.map_pre (fn ss => ss addsimprocs
+    [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
+    proc = Set_Comprehension_Pointfree.code_simproc, identifier = []}])
+*}
 
 lemma finite_induct [case_names empty insert, induct set: finite]:
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
   assumes "finite F"
   assumes "P {}"