Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorhaftmann
Thu, 26 Aug 2010 20:14:39 +0200
changeset 38785 afcc1fcb376b
parent 38783 f171050ad3f8 (diff)
parent 38784 3b4d63ab03c4 (current diff)
child 38787 948c002d773b
merged
--- 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
isabelle