--- 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;