diff -r 811c35e81ac5 -r 8601434fa334 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Jan 12 13:16:00 2014 +0100
+++ b/src/HOL/Set.thy	Sun Jan 12 14:32:22 2014 +0100
@@ -69,9 +69,9 @@
 *}
 
 simproc_setup defined_Collect ("{x. P x & Q x}") = {*
-  fn _ =>
-    Quantifier1.rearrange_Collect
-     (rtac @{thm Collect_cong} 1 THEN
+  fn _ => Quantifier1.rearrange_Collect
+    (fn _ =>
+      rtac @{thm Collect_cong} 1 THEN
       rtac @{thm iffI} 1 THEN
       ALLGOALS
         (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
@@ -355,17 +355,17 @@
 *}
 
 simproc_setup defined_Bex ("EX x:A. P x & Q x") = {*
-  let
-    val unfold_bex_tac = unfold_tac @{thms Bex_def};
-    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
-  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
+  fn _ => Quantifier1.rearrange_bex
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Bex_def} THEN
+      Quantifier1.prove_one_point_ex_tac)
 *}
 
 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
-  let
-    val unfold_ball_tac = unfold_tac @{thms Ball_def};
-    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
-  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
+  fn _ => Quantifier1.rearrange_ball
+    (fn ctxt =>
+      unfold_tac ctxt @{thms Ball_def} THEN
+      Quantifier1.prove_one_point_all_tac)
 *}
 
 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"