# HG changeset patch
# User nipkow
# Date 1676363795 -3600
# Node ID 9653bea4aa83a973a19babe4c8641cbdd355a7ea
# Parent  8bec573e1fdc4858f763a90f9855b42095e4f453# Parent  1fde0e4fd7911f7809717ed3b6b3c58014178ee5
merged

diff -r 1fde0e4fd791 -r 9653bea4aa83 NEWS
--- a/NEWS	Tue Feb 14 09:36:06 2023 +0100
+++ b/NEWS	Tue Feb 14 09:36:35 2023 +0100
@@ -226,6 +226,9 @@
 * Mirabelle:
   - Added session to output directory structure. Minor INCOMPATIBILITY.
 
+* Metis:
+  - Made clausifier more robust in the face of nested lambdas.
+
 
 *** ML ***
 
diff -r 1fde0e4fd791 -r 9653bea4aa83 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Tue Feb 14 09:36:06 2023 +0100
+++ b/src/HOL/Metis.thy	Tue Feb 14 09:36:35 2023 +0100
@@ -27,7 +27,8 @@
 lemma not_atomize_select: "(\<not> A \<Longrightarrow> select False) \<equiv> Trueprop A"
 unfolding select_def by (rule not_atomize)
 
-lemma select_FalseI: "False \<Longrightarrow> select False" by simp
+lemma select_FalseI: "False \<Longrightarrow> select False"
+by simp
 
 definition lambda :: "'a \<Rightarrow> 'a" where
 "lambda = (\<lambda>x. x)"
diff -r 1fde0e4fd791 -r 9653bea4aa83 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Feb 14 09:36:06 2023 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Feb 14 09:36:35 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 =