apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
authorhaftmann
Mon Feb 15 14:04:06 2010 +0100 (2010-02-15)
changeset 351275b29c1660047
parent 35126 ce6544f42eb9
child 35128 c1ad622e90e4
child 35156 37872c68a385
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Feb 15 14:04:06 2010 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Feb 15 14:04:06 2010 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4    in
     1.5      if target = "" then
     1.6        lthy
     1.7 -      |> direct_decl target_decl
     1.8 +      |> direct_decl global_decl
     1.9      else
    1.10        lthy
    1.11        |> pervasive ? direct_decl global_decl