--- a/src/HOL/HOL.thy Sat Oct 19 17:16:16 2024 +0200
+++ b/src/HOL/HOL.thy Sat Oct 19 19:00:19 2024 +0200
@@ -134,8 +134,8 @@
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
-print_translation \<open>
- [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Uniq\<close> \<^syntax_const>\<open>_Uniq\<close>]
+typed_print_translation \<open>
+ [(\<^const_syntax>\<open>Uniq\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
@@ -149,8 +149,8 @@
translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
-print_translation \<open>
- [Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Ex1\<close> \<^syntax_const>\<open>_Ex1\<close>]
+typed_print_translation \<open>
+ [(\<^const_syntax>\<open>Ex1\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Ex1\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>