# HG changeset patch
# User wenzelm
# Date 1176504383 -7200
# Node ID 4e2aa12af7ed12e1a299a56081e7edce60a15f62
# Parent  777af26d5713c24204add372c66c64b11dffd60c
declarations: apply target_morphism;

diff -r 777af26d5713 -r 4e2aa12af7ed src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Apr 14 00:46:22 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sat Apr 14 00:46:23 2007 +0200
@@ -280,10 +280,19 @@
 
 (* target declarations *)
 
-fun target_decl _ "" f =
-      LocalTheory.theory (Context.theory_map (f Morphism.identity)) #>
-      LocalTheory.target (Context.proof_map (f Morphism.identity))
-  | target_decl add loc f = LocalTheory.target (add loc f);
+fun target_decl add loc d lthy =
+  let
+    val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
+    val d0 = Morphism.form d';
+  in
+    if loc = "" then
+      lthy
+      |> LocalTheory.theory (Context.theory_map d0)
+      |> LocalTheory.target (Context.proof_map d0)
+    else
+      lthy
+      |> LocalTheory.target (add loc d')
+  end;
 
 val type_syntax = target_decl Locale.add_type_syntax;
 val term_syntax = target_decl Locale.add_term_syntax;