# HG changeset patch # User wenzelm # Date 1332024647 -3600 # Node ID fba03dec7cbf62b0d9e55a5fca0dc6775913062a # Parent 1c3c185bab4e22080585c2c906bac9b7421f026a amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4; diff -r 1c3c185bab4e -r fba03dec7cbf src/Pure/Isar/named_target.ML --- 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 *)