# HG changeset patch
# User ballarin
# Date 1228135412 -3600
# Node ID 7e631979922fcd9c72790f811ed3091483ca9647
# Parent  530b83967c82eed78a170e1ae10b17b98e4b915d
Methods intro_locales and unfold_locales apply to both old and new locales.

diff -r 530b83967c82 -r 7e631979922f src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 12:17:04 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 01 13:43:32 2008 +0100
@@ -167,7 +167,7 @@
 
 sublocale lgrp < right: rgrp
 print_facts
-proof new_unfold_locales
+proof unfold_locales
   {
     fix x
     have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
@@ -196,7 +196,7 @@
 (* circular interpretation *)
 
 sublocale rgrp < left: lgrp
-proof new_unfold_locales
+proof unfold_locales
   {
     fix x
     have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
@@ -225,7 +225,7 @@
     and trans: "[| x << y; y << z |] ==> x << z"
 
 sublocale order < dual: order "%x y. y << x"
-  apply new_unfold_locales apply (rule refl) apply (blast intro: trans)
+  apply unfold_locales apply (rule refl) apply (blast intro: trans)
   done
 
 print_locale! order  (* Only two instances of order. *)
@@ -244,7 +244,7 @@
 end
 
 sublocale order_with_def < dual: order' "op >>"
-  apply new_unfold_locales
+  apply unfold_locales
   unfolding greater_def
   apply (rule refl) apply (blast intro: trans)
   done
@@ -291,14 +291,14 @@
 end
 
 sublocale trivial < x: trivial x _
-  apply new_unfold_locales using Q by fast
+  apply unfold_locales using Q by fast
 
 print_locale! trivial
 
 context trivial begin thm x.Q [where ?x = True] end
 
 sublocale trivial < y: trivial Q Q
-  by new_unfold_locales
+  by unfold_locales
   (* Succeeds since previous interpretation is more general. *)
 
 print_locale! trivial  (* No instance for y created (subsumed). *)
diff -r 530b83967c82 -r 7e631979922f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Dec 01 12:17:04 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Dec 01 13:43:32 2008 +0100
@@ -2043,15 +2043,6 @@
     Method.intros_tac (wits @ intros) facts st
   end;
 
-val _ = Context.>> (Context.map_theory
-  (Method.add_methods
-    [("intro_locales",
-      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
-      "back-chain introduction rules of locales without unfolding predicates"),
-     ("unfold_locales",
-      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
-      "back-chain all introduction rules of locales")]));
-
 end;
 
 
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")]));