# HG changeset patch
# User wenzelm
# Date 1684871598 -7200
# Node ID 35439ca0133c62013cb3f91fb44fd4f9780e3eb4
# Parent  4d9349989d949ad752ef19cff183d0df2e7da053
proper setup for rule attribute;

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>