For sublocale it is sufficient to reconsider ancestors of the target.
authorballarin
Thu, 26 Aug 2010 16:00:54 +0200
changeset 38783 f171050ad3f8
parent 38782 3865cbe5d2be
child 38785 afcc1fcb376b
For sublocale it is sufficient to reconsider ancestors of the target.
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