# HG changeset patch
# User haftmann
# Date 1387308082 -3600
# Node ID e58623a33ba5a66b4b301db21bb05cec1a2ff281
# Parent  e279c2ceb54c81489b300cb45198ed48a4c9fcd4
initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts

diff -r e279c2ceb54c -r e58623a33ba5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Dec 17 15:56:57 2013 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Dec 17 20:21:22 2013 +0100
@@ -455,9 +455,16 @@
   end;
 
 fun init name thy =
-  activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of)
-    (empty_idents, Context.Proof (Proof_Context.init_global thy))
-  |-> Idents.put |> Context.proof_of;
+  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)
+  in
+    context'
+    |> Idents.put (merge_idents (marked, marked'))
+    |> Context.proof_of
+  end;
 
 
 (*** Add and extend registrations ***)