diff -r 530b83967c82 -r 7e631979922f src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Mon Dec 01 12:17:04 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Mon Dec 01 13:43:32 2008 +0100
@@ -385,11 +385,13 @@
 
 val _ = Context.>> (Context.map_theory
   (Method.add_methods
-    [("new_intro_locales",
-      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
+    [("intro_locales",
+      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt ORELSE'
+        Locale.intro_locales_tac false ctxt)),
       "back-chain introduction rules of locales without unfolding predicates"),
-     ("new_unfold_locales",
-      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
+     ("unfold_locales",
+      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
+        Locale.intro_locales_tac true ctxt)),
       "back-chain all introduction rules of locales")]));