# HG changeset patch
# User wenzelm
# Date 1146595359 -7200
# Node ID e1b81ecd4580c0e4ea05f5bbfda7ddaeb219f97b
# Parent  b5abe6cd4cbfec92acb2580d14c90059b919981b
added set_syntax_mode, restore_syntax_mode;

diff -r b5abe6cd4cbf -r e1b81ecd4580 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue May 02 20:42:37 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue May 02 20:42:39 2006 +0200
@@ -16,6 +16,8 @@
   val full_name: context -> bstring -> string
   val set_body: bool -> context -> context
   val restore_body: context -> context -> context
+  val set_syntax_mode: string * bool -> context -> context
+  val restore_syntax_mode: context -> context -> context
   val assms_of: context -> term list
   val prems_of: context -> thm list
   val fact_index_of: context -> FactIndex.T
@@ -269,6 +271,8 @@
 
 val syntax_of = #syntax o rep_context;
 val syn_of = LocalSyntax.syn_of o syntax_of;
+val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
+val restore_syntax_mode = map_syntax o LocalSyntax.restore_mode o syntax_of;
 
 val consts_of = #2 o #consts o rep_context;
 
@@ -1128,7 +1132,10 @@
     |> declare_term t
     |> map_consts
       (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode ((c, t), b)))
-    |> map_syntax (LocalSyntax.add_syntax (theory_of ctxt) (mode, inout) [(false, (c', T, mx))])
+    |> map_syntax (fn syntax => syntax
+        |> LocalSyntax.set_mode (mode, inout)
+        |> LocalSyntax.add_syntax (theory_of ctxt) [(false, (c', T, mx))]
+        |> LocalSyntax.restore_mode syntax)
   end);
 
 in
@@ -1167,7 +1174,7 @@
     ctxt'
     |> map_fixes (fn (b, fixes) => (b, rev (xs ~~ xs') @ fixes))
     |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
-    |-> (map_syntax o LocalSyntax.add_syntax thy Syntax.default_mode o map prep_mixfix)
+    |-> (map_syntax o LocalSyntax.add_syntax thy o map prep_mixfix)
     |> pair xs'
   end;