tuned;
authorwenzelm
Wed Mar 25 21:34:31 2009 +0100 (2009-03-25)
changeset 307206d8dcfb264dc
parent 30719 21c20c7d1932
child 30721 0579dec9f8ba
tuned;
src/Pure/Isar/spec_parse.ML
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Mar 25 17:23:44 2009 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Mar 25 21:34:31 2009 +0100
     1.3 @@ -112,10 +112,10 @@
     1.4  
     1.5  val locale_expression =
     1.6    let
     1.7 -    fun expr2 x = P.xname x;
     1.8 -    fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
     1.9 -      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    1.10 -    fun expr0 x = (plus1_unless locale_keyword expr1) x;
    1.11 +    val expr2 = P.xname;
    1.12 +    val expr1 = Scan.optional prefix ("", false) -- expr2 --
    1.13 +      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
    1.14 +    val expr0 = plus1_unless locale_keyword expr1;
    1.15    in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
    1.16  
    1.17  val context_element = P.group "context element" loc_element;