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