# HG changeset patch
# User wenzelm
# Date 1729357219 -7200
# Node ID 243f6bec771cbb3da25db4643da8295d45e386bc
# Parent  dff445a16252c22e2fb98257b642aa6d2f9326ad
more type information;
clarified signature;

diff -r dff445a16252 -r 243f6bec771c src/FOL/IFOL.thy
--- 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>
 
 
diff -r dff445a16252 -r 243f6bec771c src/HOL/HOL.thy
--- 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>
 
 
diff -r dff445a16252 -r 243f6bec771c src/HOL/Library/FSet.thy
--- 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
diff -r dff445a16252 -r 243f6bec771c src/HOL/Library/Multiset.thy
--- 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:
diff -r dff445a16252 -r 243f6bec771c src/HOL/Set.thy
--- 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>
diff -r dff445a16252 -r 243f6bec771c src/Pure/Syntax/syntax_trans.ML
--- 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 *)