src/Pure/Isar/spec_parse.ML
changeset 29214 76c7fc5ba849
parent 29033 721529248e31
child 29312 f369fb19146e
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Dec 12 19:58:26 2008 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Sun Dec 14 15:43:04 2008 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4  
     1.5  val rename = P.name -- Scan.option P.mixfix;
     1.6  
     1.7 -val prefix = P.name --| P.$$$ ":";
     1.8 +val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
     1.9  val named = P.name -- (P.$$$ "=" |-- P.term);
    1.10  val position = P.maybe P.term;
    1.11  val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
    1.12 @@ -127,7 +127,7 @@
    1.13  val locale_expression =
    1.14    let
    1.15      fun expr2 x = P.xname x;
    1.16 -    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    1.17 +    fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
    1.18        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    1.19      fun expr0 x = (plus1_unless locale_keyword expr1) x;
    1.20    in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;