amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
--- a/src/Pure/Isar/named_target.ML Sat Mar 17 22:46:19 2012 +0100
+++ b/src/Pure/Isar/named_target.ML Sat Mar 17 23:50:47 2012 +0100
@@ -55,12 +55,15 @@
|> Local_Theory.target (add locale locale_decl)
end;
-fun target_declaration (Target {target, ...}) {syntax, pervasive} decl =
- if target = "" then Generic_Target.theory_declaration decl
+fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
+ if target = "" then Generic_Target.theory_declaration decl lthy
else
- locale_declaration target syntax decl
- #> pervasive ? Generic_Target.theory_declaration decl
- #> not pervasive ? Context.proof_map (Morphism.form decl);
+ lthy
+ |> pervasive ? Local_Theory.background_theory
+ (Context.theory_map
+ (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl)))
+ |> locale_declaration target syntax decl
+ |> Context.proof_map (Morphism.form decl);
(* consts in locales *)