# HG changeset patch # User wenzelm # Date 1186957423 -7200 # Node ID 4bf3e084d9b56744dc658fa1becb9672d7cb6b4e # Parent d8b05073edc769b186c8eb5db3e91ce568dba14a tuned comments; diff -r d8b05073edc7 -r 4bf3e084d9b5 src/Pure/Syntax/simple_syntax.ML --- a/src/Pure/Syntax/simple_syntax.ML Mon Aug 13 00:17:57 2007 +0200 +++ b/src/Pure/Syntax/simple_syntax.ML Mon Aug 13 00:23:43 2007 +0200 @@ -57,8 +57,12 @@ (* typ = typ1 => ... => typ1 + | typ1 typ1 = typ2 const ... const - typ2 = tfree | const | "(" typ ")" + | typ2 + typ2 = tfree + | const + | ( typ ) *) fun typ x = @@ -91,7 +95,7 @@ | term5 term5 = ident | CONST const - | "(" term ")" + | ( term ) *) local