1.1 --- a/src/Pure/Isar/locale.ML	Tue Aug 05 15:07:11 2014 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Aug 05 16:21:27 2014 +0200
     1.3 @@ -448,7 +448,7 @@
     1.4    let
     1.5      val thy = Context.theory_of context;
     1.6      val activate =
     1.7 -      activate_notes Element.init
     1.8 +      activate_notes Element.init'
     1.9          (Morphism.transfer_morphism o Context.theory_of) context export;
    1.10    in
    1.11      roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
    1.12 @@ -460,7 +460,7 @@
    1.13      val context = Context.Proof (Proof_Context.init_global thy);
    1.14      val marked = Idents.get context;
    1.15      val (marked', context') = (empty_idents, context)
    1.16 -      |> activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of);
    1.17 +      |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
    1.18    in
    1.19      context'
    1.20      |> Idents.put (merge_idents (marked, marked'))