diff -r fa7c0c659798 -r 87c831e30f0a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 25 15:14:07 2012 +0200
@@ -20,7 +20,7 @@
 use "Tools/set_comprehension_pointfree.ML"
 
 simproc_setup finite_Collect ("finite (Collect P)") =
-  {* Set_Comprehension_Pointfree.simproc *}
+  {* K Set_Comprehension_Pointfree.simproc *}
 
 
 lemma finite_induct [case_names empty insert, induct set: finite]: