# HG changeset patch
# User wenzelm
# Date 1723290147 -7200
# Node ID 3d99104b4b9b51a3831335f13fdca46c87c5674b
# Parent  d517afba4968b28f5c44654385e3e198aebfe779
tuned: more antiquotations;

diff -r d517afba4968 -r 3d99104b4b9b src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 13:42:16 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 13:42:27 2024 +0200
@@ -455,7 +455,7 @@
 *)
 fun lambda_prs_simple_conv ctxt ctrm =
   (case Thm.term_of ctrm of
-    (Const (\<^const_name>\<open>map_fun\<close>, _) $ r1 $ a2) $ (Abs _) =>
+     \<^Const_>\<open>map_fun _ _ _ _ for r1 a2 \<open>Abs _\<close>\<close> =>
       let
         val (ty_b, ty_a) = dest_funT (fastype_of r1)
         val (ty_c, ty_d) = dest_funT (fastype_of a2)