Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper setup for rule attribute;
authorwenzelm
Tue, 23 May 2023 21:53:18 +0200
changeset 78100 35439ca0133c
parent 78099 4d9349989d94
child 78101 300537844bb7
proper setup for rule attribute;
src/HOL/Decision_Procs/Conversions.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle