--- a/src/Pure/Isar/context_rules.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Isar/context_rules.ML Wed Dec 06 18:59:33 2017 +0100
@@ -219,13 +219,13 @@
Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
val _ = Theory.setup
- (Attrib.setup @{binding intro} (add intro_bang intro intro_query)
+ (Attrib.setup \<^binding>\<open>intro\<close> (add intro_bang intro intro_query)
"declaration of introduction rule" #>
- Attrib.setup @{binding elim} (add elim_bang elim elim_query)
+ Attrib.setup \<^binding>\<open>elim\<close> (add elim_bang elim elim_query)
"declaration of elimination rule" #>
- Attrib.setup @{binding dest} (add dest_bang dest dest_query)
+ Attrib.setup \<^binding>\<open>dest\<close> (add dest_bang dest dest_query)
"declaration of destruction rule" #>
- Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+ Attrib.setup \<^binding>\<open>rule\<close> (Scan.lift Args.del >> K rule_del)
"remove declaration of intro/elim/dest rule");
end;