src/Pure/Isar/theory_target.ML
changeset 35127 5b29c1660047
parent 33764 7bcefaab8d41
child 35205 611b90bb89bc
     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