--- a/src/Pure/Isar/named_target.ML Thu Mar 22 11:11:51 2012 +0100
+++ b/src/Pure/Isar/named_target.ML Thu Mar 22 15:41:49 2012 +0100
@@ -61,12 +61,10 @@
end;
fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
- if target = "" then Generic_Target.theory_declaration decl lthy
+ if target = "" then Generic_Target.standard_declaration decl lthy
else
lthy
- |> pervasive ? Local_Theory.background_theory
- (Context.theory_map
- (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl)))
+ |> pervasive ? Generic_Target.background_declaration decl
|> locale_declaration target syntax decl
|> Context.proof_map (Morphism.form decl);