--- a/src/Pure/Isar/isar_syn.ML Wed Jun 09 18:52:55 2004 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jun 09 18:53:13 2004 +0200
@@ -140,7 +140,8 @@
val mode_spec =
(P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
-val opt_mode = Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) ("", true);
+val opt_mode =
+ Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
val syntaxP =
OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl