src/Pure/Isar/isar_syn.ML
changeset 24960 39d1dd215d73
parent 24953 f92386569176
child 25003 0b067b2d1b88
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 11 16:05:23 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 11 16:05:26 2007 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4    (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
     1.5  
     1.6  val opt_mode =
     1.7 -  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.default_mode;
     1.8 +  Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.mode_default;
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl