# HG changeset patch
# User wenzelm
# Date 1117533197 -7200
# Node ID 3ba9eb7ea3667c69aa774c1bca2331a9de2476b8
# Parent  bd13a0017137756b52248ba9090fd4ee432240a4
fixed outer syntax: allow type_args with parentheses;

diff -r bd13a0017137 -r 3ba9eb7ea366 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue May 31 11:53:16 2005 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue May 31 11:53:17 2005 +0200
@@ -375,9 +375,9 @@
 
 
 val typedef_proof_decl =
-  Scan.optional (P.$$$ "(" |-- P.!!!
-      (((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
-        --| P.$$$ ")")) (true, NONE) --
+  Scan.optional (P.$$$ "(" |--
+      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+        --| P.$$$ ")") (true, NONE) --
     (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));