src/HOL/Set.thy

 Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"}
 to the front (and similarly for @{text "t=x"}):
 *}
 
 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}]))
 *}
 

     end;
   in [(@{const_syntax Collect}, setcompr_tr')] end;
 *}
 
 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"
   by (simp add: Ball_def)