--- a/src/Pure/Isar/locale.ML Tue Mar 18 13:36:28 2014 +0100
+++ b/src/Pure/Isar/locale.ML Tue Mar 18 15:29:58 2014 +0100
@@ -622,9 +622,9 @@
val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
val _ = Theory.setup
- (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
+ (Method.setup @{binding intro_locales} (Scan.succeed (METHOD o try_intro_locales_tac false))
"back-chain introduction rules of locales without unfolding predicates" #>
- Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
+ Method.setup @{binding unfold_locales} (Scan.succeed (METHOD o try_intro_locales_tac true))
"back-chain all introduction rules of locales");