tuned comments;
authorwenzelm
Mon Aug 13 00:23:43 2007 +0200 (2007-08-13)
changeset 242374bf3e084d9b5
parent 24236 d8b05073edc7
child 24238 ae70f95e31de
tuned comments;
src/Pure/Syntax/simple_syntax.ML
     1.1 --- a/src/Pure/Syntax/simple_syntax.ML	Mon Aug 13 00:17:57 2007 +0200
     1.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Mon Aug 13 00:23:43 2007 +0200
     1.3 @@ -57,8 +57,12 @@
     1.4  
     1.5  (*
     1.6    typ  = typ1 => ... => typ1
     1.7 +       | typ1
     1.8    typ1 = typ2 const ... const
     1.9 -  typ2 = tfree | const | "(" typ ")"
    1.10 +       | typ2
    1.11 +  typ2 = tfree
    1.12 +       | const
    1.13 +       | ( typ )
    1.14  *)
    1.15  
    1.16  fun typ x =
    1.17 @@ -91,7 +95,7 @@
    1.18          | term5
    1.19    term5 = ident
    1.20          | CONST const
    1.21 -        | "(" term ")"
    1.22 +        | ( term )
    1.23  *)
    1.24  
    1.25  local