--- a/src/HOL/Tools/Meson/meson_clausify.ML Sun Feb 12 22:05:02 2023 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Feb 13 15:01:58 2023 +0100
@@ -54,8 +54,21 @@
let val T = fastype_of t
in \<^Const>\<open>Meson.skolem T for t\<close> end
+fun eta_expand_All_Ex_arg ((cst as (Const _)) $ Abs (s, T, t')) =
+ cst $ Abs (s, T, eta_expand_All_Ex_arg t')
+ | eta_expand_All_Ex_arg ((cst as (Const (cst_s, cst_T))) $ t') =
+ if member (op =) [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>] cst_s then
+ cst $ Abs (Name.uu, domain_type (domain_type cst_T),
+ incr_boundvars 1 (eta_expand_All_Ex_arg t') $ Bound 0)
+ else
+ cst $ eta_expand_All_Ex_arg t'
+ | eta_expand_All_Ex_arg (Abs (s, T, t')) = Abs (s, T, eta_expand_All_Ex_arg t')
+ | eta_expand_All_Ex_arg (t1 $ t2) =
+ eta_expand_All_Ex_arg t1 $ eta_expand_All_Ex_arg t2
+ | eta_expand_All_Ex_arg t = t
+
fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
- | beta_eta_in_abs_body t = Envir.beta_eta_contract t
+ | beta_eta_in_abs_body t = eta_expand_All_Ex_arg (Envir.beta_eta_contract t)
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun old_skolem_defs th =