# HG changeset patch
# User wenzelm
# Date 1165683949 -3600
# Node ID 7b3ccdae92122994545dc9c797383798231dbd5c
# Parent  906649272ba0dff60e5b40f63c2dd1a4eb559103
TermSyntax.abbrev;
ProofContext.set_expand_abbrevs;

diff -r 906649272ba0 -r 7b3ccdae9212 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Dec 09 18:05:48 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Dec 09 18:05:49 2006 +0100
@@ -146,14 +146,14 @@
   let
     val ((vars, [(_, [prop])]), _) =
       prep (the_list raw_var) [(("", []), [raw_prop])]
-        (lthy |> ProofContext.expand_abbrevs false);
+        (lthy |> ProofContext.set_expand_abbrevs false);
     val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
     val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
       if x = y then mx
       else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     val lthy' = lthy
       |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
-      |> TermSyntax.abbrevs mode [((x, mx), rhs)]
+      |> TermSyntax.abbrev mode ((x, mx), rhs)
       |> ProofContext.restore_syntax_mode lthy;
     val _ = print_consts lthy' (K false) [(x, T)]
   in lthy' end;