src/Pure/Isar/locale.ML

     val (dependencies, marked') = add thy 0 (name, morph) ([], []);
     (* Filter out exisiting fragments. *)
     val dependencies' = filter_out (fn (name, morph) =>
       member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
   in
-    (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
+    (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
   end;
 
 end;
 
 

       (* FIXME type parameters *)
       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
         else I);
-  in
-    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
+    val activate = activate_notes activ_elem transfer thy;
+  in
+    roundup thy activate (name, Morphism.identity) (marked, input')
   end;
 
 
 (** Public activation functions **)
 

 
 fun activate_declarations dep ctxt =
   let
     val context = Context.Proof ctxt;
     val thy = Context.theory_of context;
-    val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
+    val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
   in Context.the_proof context' end;
 
 fun activate_facts dep context =
   let
     val thy = Context.theory_of context;
-    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
+    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of) thy;
   in roundup thy activate dep (get_idents context, context) |-> put_idents end;
 
 fun init name thy =
   activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
     ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;

 
 val get_registrations =
   Registrations.get #> map (#1 #> apsnd op $>);
 
 fun add_registration (name, (base_morph, export)) thy =
-  roundup thy (fn _ => fn (name', morph') =>
-    Registrations.map (cons ((name', (morph', export)), stamp ())))
+  roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
     (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
     (* FIXME |-> put_global_idents ?*)
 
 fun amend_registration morph (name, base_morph) thy =
   let