1.1 --- a/src/Pure/Isar/specification.ML	Tue Dec 12 17:29:26 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Tue Dec 12 20:49:19 2006 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4        else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
     1.5      val lthy' = lthy
     1.6        |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
     1.7 -      |> LocalTheory.abbrev mode ((x, mx), rhs)
     1.8 +      |> LocalTheory.abbrev mode ((x, mx), rhs) |> snd
     1.9        |> ProofContext.restore_syntax_mode lthy;
    1.10      val _ = print_consts lthy' (K false) [(x, T)]
    1.11    in lthy' end;