src/Pure/Isar/isar_syn.ML

 val abbreviationP =
   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
     (P.opt_locale_target -- opt_mode --
       Scan.repeat1 (Scan.option constdecl -- P.prop)
     >> (fn ((loc, mode), args) =>
-        Toplevel.local_theory loc (Specification.abbreviation mode args)));
+        Toplevel.local_theory loc (snd o Specification.abbreviation mode args)));
 
 val notationP =
   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
     (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
     >> (fn ((loc, mode), args) =>