# HG changeset patch
# User ballarin
# Date 1282831254 -7200
# Node ID f171050ad3f843bad95b501f71ae12c437568845
# Parent  3865cbe5d2be2456ee579a40ce6fd7c393091c62
For sublocale it is sufficient to reconsider ancestors of the target.

diff -r 3865cbe5d2be -r f171050ad3f8 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 26 14:04:13 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 26 16:00:54 2010 +0200
@@ -483,7 +483,7 @@
     val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
     val context' = Context.Theory thy';
     val (_, regs) = fold_rev (roundup thy' cons export)
-      (all_registrations context') (get_idents (context'), []);
+      (registrations_of context' loc) (get_idents (context'), []);
   in
     thy'
     |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs