# HG changeset patch
# User wenzelm
# Date 1194787035 -3600
# Node ID e83bef45e6a7003c0830e26ec10d1e382b6eb020
# Parent  db25c98f32e1ebf2f9dffffac6be8a167e1f234f
abbrev: back to PrintMode.internal, which works at least half-way;

diff -r db25c98f32e1 -r e83bef45e6a7 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Nov 11 14:00:13 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Nov 11 14:17:15 2007 +0100
@@ -219,7 +219,7 @@
   in
     lthy |>
      (if is_locale then
-        LocalTheory.theory_result (Sign.add_abbrev PrintMode.input pos (c, global_rhs))
+        LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal pos (c, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
             term_syntax ta (locale_const ta prmode pos ((c, mx2), lhs')) #>