# HG changeset patch
# User haftmann
# Date 1266239046 -3600
# Node ID 5b29c166004761bb7424983c94d2a9202ae03248
# Parent  ce6544f42eb9807ad951a04b78f1195dd91faa6c
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target

diff -r ce6544f42eb9 -r 5b29c1660047 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Feb 15 14:04:06 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Feb 15 14:04:06 2010 +0100
@@ -88,7 +88,7 @@
   in
     if target = "" then
       lthy
-      |> direct_decl target_decl
+      |> direct_decl global_decl
     else
       lthy
       |> pervasive ? direct_decl global_decl