simplified roundup activation interface;

--- a/src/Pure/Isar/locale.ML	Sat Mar 28 20:52:52 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Mar 29 16:13:24 2009 +0200
@@ -245,7 +245,7 @@
     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;
@@ -285,8 +285,9 @@
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
         else I);
+    val activate = activate_notes activ_elem transfer thy;
   in
-    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
+    roundup thy activate (name, Morphism.identity) (marked, input')
   end;
 
 
@@ -327,13 +328,13 @@
   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 =
@@ -375,8 +376,7 @@
   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 ?*)