# HG changeset patch
# User wenzelm
# Date 1086799993 -7200
# Node ID c66394c408f7f6fef81960cd105f4108d40befd1
# Parent  d9b6c81b52acd5095e78044760ff9aae90781a74
Syntax.default_mode;

diff -r d9b6c81b52ac -r c66394c408f7 src/Pure/Isar/isar_syn.ML
--- 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
diff -r d9b6c81b52ac -r c66394c408f7 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Wed Jun 09 18:52:55 2004 +0200
+++ b/src/Pure/goals.ML	Wed Jun 09 18:53:13 2004 +0200
@@ -507,7 +507,7 @@
 
     val syntax_thy =
       thy
-      |> Theory.add_modesyntax_i ("", true) loc_syn
+      |> Theory.add_modesyntax_i Syntax.default_mode loc_syn
       |> Theory.add_trfuns ([], loc_trfuns, [], []);
 
     val syntax_sign = Theory.sign_of syntax_thy;