# HG changeset patch
# User wenzelm
# Date 1683748028 -7200
# Node ID 51d135645d701f7cd37a240f8bc3cc0fbda5f8c8
# Parent  261b527f1b03009ca841ccbbf0eacf43110089d9
tuned;

diff -r 261b527f1b03 -r 51d135645d70 src/HOL/Tools/SMT/z3_replay_rules.ML
--- a/src/HOL/Tools/SMT/z3_replay_rules.ML	Wed May 10 21:41:58 2023 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_rules.ML	Wed May 10 21:47:08 2023 +0200
@@ -43,11 +43,8 @@
 val add = Thm.declaration_attribute (Data.map o ins)
 val del = Thm.declaration_attribute (Data.map o del)
 
-val name = Binding.name "z3_rule"
-
-val description = "declaration of Z3 proof rules"
-
-val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
-  Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
+val _ = Theory.setup
+ (Attrib.setup \<^binding>\<open>z3_rule\<close> (Attrib.add_del add del) "declaration of Z3 proof rules" #>
+  Global_Theory.add_thms_dynamic (\<^binding>\<open>z3_rule\<close>, Net.content o Data.get))
 
 end;