diff -r 4d9349989d94 -r 35439ca0133c src/HOL/Decision_Procs/Conversions.thy
--- a/src/HOL/Decision_Procs/Conversions.thy	Tue May 23 21:43:36 2023 +0200
+++ b/src/HOL/Decision_Procs/Conversions.thy	Tue May 23 21:53:18 2023 +0200
@@ -20,7 +20,7 @@
 \<close>
 
 attribute_setup meta =
-  \<open>Scan.succeed (fn (ctxt, th) => (NONE, SOME (mk_meta_eq th)))\<close>
+  \<open>Scan.succeed (Thm.rule_attribute [] (K mk_meta_eq))\<close>
   \<open>convert equality to meta equality\<close>
 
 ML \<open>