--- a/src/Pure/Isar/locale.ML Wed Dec 06 15:46:35 2017 +0100
+++ b/src/Pure/Isar/locale.ML Wed Dec 06 18:59:33 2017 +0100
@@ -678,9 +678,9 @@
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
val _ = Theory.setup
- (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false))
+ (Method.setup \<^binding>\<open>intro_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac false))
"back-chain introduction rules of locales without unfolding predicates" #>
- Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
+ Method.setup \<^binding>\<open>unfold_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac true))
"back-chain all introduction rules of locales");