1.1 --- a/src/Pure/Isar/named_target.ML	Sat Mar 17 22:46:19 2012 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sat Mar 17 23:50:47 2012 +0100
     1.3 @@ -55,12 +55,15 @@
     1.4      |> Local_Theory.target (add locale locale_decl)
     1.5    end;
     1.6  
     1.7 -fun target_declaration (Target {target, ...}) {syntax, pervasive} decl =
     1.8 -  if target = "" then Generic_Target.theory_declaration decl
     1.9 +fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
    1.10 +  if target = "" then Generic_Target.theory_declaration decl lthy
    1.11    else
    1.12 -    locale_declaration target syntax decl
    1.13 -    #> pervasive ? Generic_Target.theory_declaration decl
    1.14 -    #> not pervasive ? Context.proof_map (Morphism.form decl);
    1.15 +    lthy
    1.16 +    |> pervasive ? Local_Theory.background_theory
    1.17 +        (Context.theory_map
    1.18 +          (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl)))
    1.19 +    |> locale_declaration target syntax decl
    1.20 +    |> Context.proof_map (Morphism.form decl);
    1.21  
    1.22  
    1.23  (* consts in locales *)