src/HOL/Set.thy
changeset 81202 243f6bec771c
parent 81182 fc5066122e68
child 81473 53e61087bc6f
--- a/src/HOL/Set.thy	Sat Oct 19 17:16:16 2024 +0200
+++ b/src/HOL/Set.thy	Sat Oct 19 19:00:19 2024 +0200
@@ -323,9 +323,9 @@
   in [(\<^syntax_const>\<open>_Setcompr\<close>, setcompr_tr)] end
 \<close>
 
-print_translation \<open>
- [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Ball\<close> \<^syntax_const>\<open>_Ball\<close>,
-  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Bex\<close> \<^syntax_const>\<open>_Bex\<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>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 print_translation \<open>