src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 09 18:58:52 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 09 21:44:27 2006 +0100
@@ -221,7 +221,7 @@
     (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