# HG changeset patch # User haftmann # Date 1282846479 -7200 # Node ID afcc1fcb376b134758594f985f905f4e0fb102dc # Parent f171050ad3f843bad95b501f71ae12c437568845# Parent 3b4d63ab03c49de777d5452b5e21d39a2070e935 merged diff -r 3b4d63ab03c4 -r afcc1fcb376b src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Aug 26 20:14:24 2010 +0200 +++ b/src/Pure/Isar/locale.ML Thu Aug 26 20:14:39 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