1.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 20:52:52 2009 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 29 16:13:24 2009 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4      val dependencies' = filter_out (fn (name, morph) =>
     1.5        member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
     1.6    in
     1.7 -    (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
     1.8 +    (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
     1.9    end;
    1.10  
    1.11  end;
    1.12 @@ -285,8 +285,9 @@
    1.13        (if not (null defs)
    1.14          then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
    1.15          else I);
    1.16 +    val activate = activate_notes activ_elem transfer thy;
    1.17    in
    1.18 -    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
    1.19 +    roundup thy activate (name, Morphism.identity) (marked, input')
    1.20    end;
    1.21  
    1.22  
    1.23 @@ -327,13 +328,13 @@
    1.24    let
    1.25      val context = Context.Proof ctxt;
    1.26      val thy = Context.theory_of context;
    1.27 -    val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
    1.28 +    val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
    1.29    in Context.the_proof context' end;
    1.30  
    1.31  fun activate_facts dep context =
    1.32    let
    1.33      val thy = Context.theory_of context;
    1.34 -    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
    1.35 +    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of) thy;
    1.36    in roundup thy activate dep (get_idents context, context) |-> put_idents end;
    1.37  
    1.38  fun init name thy =
    1.39 @@ -375,8 +376,7 @@
    1.40    Registrations.get #> map (#1 #> apsnd op $>);
    1.41  
    1.42  fun add_registration (name, (base_morph, export)) thy =
    1.43 -  roundup thy (fn _ => fn (name', morph') =>
    1.44 -    Registrations.map (cons ((name', (morph', export)), stamp ())))
    1.45 +  roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
    1.46      (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
    1.47      (* FIXME |-> put_global_idents ?*)
    1.48