# 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