src/Pure/Isar/new_locale.ML

   val add_dependency: string -> (string * Morphism.morphism) -> theory -> theory
 
   (* Activation *)
   val activate_declarations: theory -> string * Morphism.morphism ->
     Proof.context -> Proof.context
-  val activate_global_facts: string * Morphism.morphism ->
-    theory -> theory
-  val activate_local_facts: theory -> string * Morphism.morphism ->
-    Proof.context -> Proof.context
+  val activate_global_facts: string * Morphism.morphism -> theory -> theory
+  val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
 (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)
   val witness_attrib: attribute

   
 fun activate_global_facts dep thy =
   roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
   uncurry put_global_idents;
 
-fun activate_local_facts thy dep ctxt =
-  roundup thy (activate_notes init_local_elem) dep (get_local_idents ctxt, ctxt) |>
+fun activate_local_facts dep ctxt =
+  roundup (ProofContext.theory_of ctxt) (activate_notes init_local_elem) dep
+    (get_local_idents ctxt, ctxt) |>
   uncurry put_local_idents;
 
 fun init name thy = activate_all name thy init_local_elem (empty, ProofContext.init thy) |>
   uncurry put_local_idents;
 

       Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt ORELSE'
         Locale.intro_locales_tac true ctxt)),
       "back-chain all introduction rules of locales")]));
 
 
-(*** Registrations: interpretations in theories and proof contexts ***)
-
+(*** Registrations: interpretations in theories ***)
+
+(* FIXME only global variant needed *)
 structure RegistrationsData = GenericDataFun
 (
   type T = ((string * Morphism.morphism) * stamp) list;
     (* registrations, in reverse order of declaration *)
   val empty = [];

 
 val get_global_registrations = map fst o RegistrationsData.get o Context.Theory;
 fun add_global_registration reg =
   (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
 
-
-end;
-
+end;
+