--- 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)));