# HG changeset patch
# User wenzelm
# Date 1166021256 -3600
# Node ID 6f6bf23f4c1e6331763c182b1ed16164cf70579b
# Parent  153fad1e7318bbea07f8138639511f37c8721c0e
internal_abbrev: observe print mode;

diff -r 153fad1e7318 -r 6f6bf23f4c1e src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Dec 13 15:47:34 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Dec 13 15:47:36 2006 +0100
@@ -64,9 +64,9 @@
     val mx2 = if is_loc then mx else NoSyn;
   in (mx1, mx2) end;
 
-fun internal_abbrev ((c, mx), t) =
-  LocalTheory.term_syntax (ProofContext.target_abbrev Syntax.internal_mode ((c, mx), t)) #>
-  ProofContext.add_abbrev (#1 Syntax.internal_mode) (c, t) #> snd;
+fun internal_abbrev prmode ((c, mx), t) =
+  LocalTheory.term_syntax (ProofContext.target_abbrev prmode ((c, mx), t)) #>
+  ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
 
 fun consts is_class is_loc depends decls lthy =
   let
@@ -84,7 +84,7 @@
     val defs = map (apsnd (pair ("", []))) abbrs;
   in
     lthy'
-    |> is_loc ? fold internal_abbrev abbrs
+    |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs
     |> LocalDefs.add_defs defs |>> map (apsnd snd)
   end;
 
@@ -114,7 +114,7 @@
   in
     lthy1
     |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
-    |> is_loc ? internal_abbrev ((c, mx2), Term.list_comb (Const (full_c, U), xs))
+    |> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
     |> ProofContext.local_abbrev (c, rhs)
   end;