# HG changeset patch # User wenzelm # Date 1391431554 -3600 # Node ID 0594b429baf9e9d59cc52f64cd1ec2f4452c9381 # Parent 765555d6a0b29fff154193921793dd304c41c926 tuned; diff -r 765555d6a0b2 -r 0594b429baf9 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Feb 03 13:35:50 2014 +0100 +++ b/src/Pure/Isar/locale.ML Mon Feb 03 13:45:54 2014 +0100 @@ -458,8 +458,8 @@ let val context = Context.Proof (Proof_Context.init_global thy); val marked = Idents.get context; - val (marked', context') = activate_all name thy Element.init - (Morphism.transfer_morphism o Context.theory_of) (empty_idents, context) + val (marked', context') = (empty_idents, context) + |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of); in context' |> Idents.put (merge_idents (marked, marked'))