abbrev: PrintMode.input instead of PrintMode.internal for global version!
authorwenzelm
Sun Nov 11 14:00:11 2007 +0100 (2007-11-11)
changeset 25392bb8d225dcf05
parent 25391 783e5de2a6c7
child 25393 0856e0141062
abbrev: PrintMode.input instead of PrintMode.internal for global version!
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sun Nov 11 14:00:10 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Nov 11 14:00:11 2007 +0100
     1.3 @@ -219,7 +219,7 @@
     1.4    in
     1.5      lthy |>
     1.6       (if is_locale then
     1.7 -        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal pos (c, global_rhs))
     1.8 +        LocalTheory.theory_result (Sign.add_abbrev PrintMode.input pos (c, global_rhs))
     1.9          #-> (fn (lhs, _) =>
    1.10            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    1.11              term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>