For sublocale it is sufficient to reconsider ancestors of the target.
authorballarin
Thu, 26 Aug 2010 16:00:54 +0200
changeset 39016f171050ad3f8
parent 39015 3865cbe5d2be
child 39018 afcc1fcb376b
For sublocale it is sufficient to reconsider ancestors of the target.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 26 14:04:13 2010 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 26 16:00:54 2010 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4      val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
     1.5      val context' = Context.Theory thy';
     1.6      val (_, regs) = fold_rev (roundup thy' cons export)
     1.7 -      (all_registrations context') (get_idents (context'), []);
     1.8 +      (registrations_of context' loc) (get_idents (context'), []);
     1.9    in
    1.10      thy'
    1.11      |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs