# HG changeset patch
# User wenzelm
# Date 1144529483 -7200
# Node ID 27cf4802aa18c3772a84979e0866b2ee51788c6d
# Parent  6af9ee48b563a9c18530816d9050546a2c6e6678
'abbreviation': optional print mode;

diff -r 6af9ee48b563 -r 27cf4802aa18 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Apr 08 22:51:22 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 08 22:51:23 2006 +0200
@@ -209,8 +209,7 @@
 
 val abbreviationP =
   OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
-    (P.opt_locale_target --
-      Scan.optional (P.$$$ "(" -- P.$$$ "output" -- P.$$$ ")" >> K true) false --
+    (P.opt_locale_target -- opt_mode --
       Scan.repeat1 (Scan.option constdecl -- P.prop)
     >> (fn ((loc, revert), args) =>
          Toplevel.local_theory loc (Specification.abbreviation revert args)));