# HG changeset patch
# User wenzelm
# Date 1146595360 -7200
# Node ID e3a39dae2004cd7f19f2ff362cae1b8cc236546a
# Parent  e1b81ecd4580c0e4ea05f5bbfda7ddaeb219f97b
abbreviation: observe local syntax mode;

diff -r e1b81ecd4580 -r e3a39dae2004 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue May 02 20:42:39 2006 +0200
+++ b/src/Pure/Isar/specification.ML	Tue May 02 20:42:40 2006 +0200
@@ -111,7 +111,7 @@
 
 (* abbreviation *)
 
-fun gen_abbrevs prep prmode args ctxt =
+fun gen_abbrevs prep mode args ctxt =
   let
     fun abbrev (raw_var, raw_prop) ctxt' =
       let
@@ -124,11 +124,14 @@
           else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote x'));
       in
         ctxt'
-        |> LocalTheory.abbrev prmode ((x, mx), rhs)
+        |> LocalTheory.abbrev mode ((x, mx), rhs)
         |> pair (x, T)
       end;
 
-    val (cs, abbrs_ctxt) = ctxt |> fold_map abbrev args;
+    val (cs, abbrs_ctxt) = ctxt
+      |> ProofContext.set_syntax_mode mode
+      |> fold_map abbrev args
+      ||> ProofContext.restore_syntax_mode ctxt;
     val _ = LocalTheory.print_consts ctxt (K false) cs;
   in abbrs_ctxt end;