# HG changeset patch
# User wenzelm
# Date 1634049043 -7200
# Node ID 907483081d4c571ae755d62ecad7d0546159b90f
# Parent  0803dd7f920db487634dfdc279bd74db5f4b3e39
prefer standard Term.dest_abs, with minor deviation of generated names;

diff -r 0803dd7f920d -r 907483081d4c src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 12 16:12:41 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Tue Oct 12 16:30:43 2021 +0200
@@ -71,10 +71,7 @@
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
-      | dec_sko \<^Const_>\<open>All _ for \<open>Abs (a, T, p)\<close>\<close> rhss =
-        (*Universal quant: insert a free variable into body and continue*)
-        let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
-        in dec_sko (subst_bound (Free(fname,T), p)) rhss end
+      | dec_sko \<^Const_>\<open>All _ for \<open>Abs abs\<close>\<close> rhss = dec_sko (#2 (Term.dest_abs abs)) rhss
       | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
       | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss