--- a/src/FOL/IFOL.thy Sat Oct 19 17:16:16 2024 +0200
+++ b/src/FOL/IFOL.thy Sat Oct 19 19:00:19 2024 +0200
@@ -104,9 +104,8 @@
syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o" (\<open>(\<open>indent=2 notation=\<open>binder \<exists>\<^sub>\<le>\<^sub>1\<close>\<close>\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
syntax_consts "_Uniq" \<rightleftharpoons> Uniq
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>
--- 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>
--- a/src/HOL/Library/FSet.thy Sat Oct 19 17:16:16 2024 +0200
+++ b/src/HOL/Library/FSet.thy Sat Oct 19 19:00:19 2024 +0200
@@ -215,9 +215,9 @@
"\<nexists>x|\<in>|A. P" \<rightleftharpoons> "CONST fBall A (\<lambda>x. \<not> P)"
"\<exists>!x|\<in>|A. P" \<rightharpoonup> "\<exists>!x. x |\<in>| A \<and> P"
-print_translation \<open>
- [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBall\<close> \<^syntax_const>\<open>_fBall\<close>,
- Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBex\<close> \<^syntax_const>\<open>_fBex\<close>]
+typed_print_translation \<open>
+ [(\<^const_syntax>\<open>fBall\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBall\<close>),
+ (\<^const_syntax>\<open>fBex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBex\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
syntax
--- a/src/HOL/Library/Multiset.thy Sat Oct 19 17:16:16 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Oct 19 19:00:19 2024 +0200
@@ -180,9 +180,9 @@
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
-print_translation \<open>
- [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Ball\<close> \<^syntax_const>\<open>_MBall\<close>,
- Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Bex\<close> \<^syntax_const>\<open>_MBex\<close>]
+typed_print_translation \<open>
+ [(\<^const_syntax>\<open>Multiset.Ball\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBall\<close>),
+ (\<^const_syntax>\<open>Multiset.Bex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBex\<close>)]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
lemma count_eq_zero_iff:
--- 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>
--- a/src/Pure/Syntax/syntax_trans.ML Sat Oct 19 17:16:16 2024 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Sat Oct 19 19:00:19 2024 +0200
@@ -36,8 +36,8 @@
val atomic_abs_tr': string * typ * term -> term * term
val const_abs_tr': term -> term
val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
- val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
- val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
+ val preserve_binder_abs_tr': string -> typ -> term list -> term
+ val preserve_binder_abs2_tr': string -> typ -> term list -> term
val print_abs: string * typ * term -> string * term
val dependent_tr': string * string -> term list -> term
val antiquote_tr': string -> term -> term
@@ -355,13 +355,13 @@
| binder_tr' [] = raise Match;
in (name, fn _ => binder_tr') end;
-fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
+fun preserve_binder_abs_tr' syn ty (Abs abs :: ts) =
let val (x, t) = atomic_abs_tr' abs
- in list_comb (Syntax.const syn $ x $ t, ts) end);
+ in list_comb (Const (syn, ty) $ x $ t, ts) end;
-fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
+fun preserve_binder_abs2_tr' syn ty (A :: Abs abs :: ts) =
let val (x, t) = atomic_abs_tr' abs
- in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
+ in list_comb (Const (syn, ty) $ x $ A $ t, ts) end;
(* idtyp constraints *)