src/HOL/Set.thy

 
   in [(\<^syntax_const>\<open>_Setcompr\<close>, setcompr_tr)] end
 \<close>
 
 typed_print_translation \<open>
- [(\<^const_syntax>\<open>Ball\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
-  (\<^const_syntax>\<open>Bex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
+ [(\<^const_syntax>\<open>Ball\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
+  (\<^const_syntax>\<open>Bex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 print_translation \<open>
 let
   val ex_tr' = snd (Syntax_Trans.mk_binder_tr' (\<^const_syntax>\<open>Ex\<close>, "DUMMY"));

           in Syntax.const \<^syntax_const>\<open>_Setcompr\<close> $ e $ idts $ Q end;
     in
       if check (P, 0) then tr' P
       else
         let
-          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
+          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
           val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
         in
           case t of
             Const (\<^const_syntax>\<open>HOL.conj\<close>, _) $
               (Const (\<^const_syntax>\<open>Set.member\<close>, _) $