fixed outer syntax: allow type_args with parentheses;
authorwenzelm
Tue May 31 11:53:17 2005 +0200 (2005-05-31)
changeset 161263ba9eb7ea366
parent 16125 bd13a0017137
child 16127 549fff1d0fc6
fixed outer syntax: allow type_args with parentheses;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Tue May 31 11:53:16 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue May 31 11:53:17 2005 +0200
     1.3 @@ -375,9 +375,9 @@
     1.4  
     1.5  
     1.6  val typedef_proof_decl =
     1.7 -  Scan.optional (P.$$$ "(" |-- P.!!!
     1.8 -      (((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
     1.9 -        --| P.$$$ ")")) (true, NONE) --
    1.10 +  Scan.optional (P.$$$ "(" |--
    1.11 +      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
    1.12 +        --| P.$$$ ")") (true, NONE) --
    1.13      (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    1.14      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    1.15