# HG changeset patch
# User wenzelm
# Date 1390426348 -3600
# Node ID 9ca72949ebac199f06ffa5065de0577e8fa80446
# Parent  7df949045dc5436a3bdc9dd730cb490a67408514
observe local syntax mode (according to e3a39dae2004, which was lost in 0f3ad56548bc), e.g. relevant for "abbreviation (output)" with non-terminating syntax;

diff -r 7df949045dc5 -r 9ca72949ebac src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Jan 22 21:33:50 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Jan 22 22:32:28 2014 +0100
@@ -234,10 +234,12 @@
 
 fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
   let
+    val lthy1 = lthy
+      |> Proof_Context.set_syntax_mode mode;
     val ((vars, [(_, prop)]), _) =
       prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
-        (lthy |> Proof_Context.set_mode Proof_Context.mode_abbrev);
-    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
+        (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
+    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
     val var =
       (case vars of
         [] => (Binding.name x, NoSyn)
@@ -248,13 +250,12 @@
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.here (Binding.pos_of b));
           in (b, mx) end);
-    val lthy' = lthy
-      |> Proof_Context.set_syntax_mode mode    (* FIXME ?!? *)
+    val lthy2 = lthy1
       |> Local_Theory.abbrev mode (var, rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
 
-    val _ = Proof_Display.print_consts int lthy' (K false) [(x, T)];
-  in lthy' end;
+    val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)];
+  in lthy2 end;
 
 val abbreviation = gen_abbrev check_free_spec;
 val abbreviation_cmd = gen_abbrev read_free_spec;