| changeset 24014 | d3873741678d |
| parent 24013 | 3063a756611d |
| child 24869 | bad2b2be1f24 |
--- a/src/Pure/Isar/spec_parse.ML Fri Jul 27 21:55:23 2007 +0200 +++ b/src/Pure/Isar/spec_parse.ML Fri Jul 27 22:19:49 2007 +0200 @@ -52,7 +52,7 @@ (* theorem specifications *) val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src; -val attribs = P.$$$ "[" |-- P.!!! (P.list attrib --| P.$$$ "]"); +val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]"; val opt_attribs = Scan.optional attribs []; fun thm_name s = P.name -- opt_attribs --| P.$$$ s;