| changeset 27378 | 0968c0d0b969 |
| parent 26361 | 7946f459c6c8 |
| child 27816 | 0dfed2f2822a |
--- a/src/Pure/Isar/spec_parse.ML Sat Jun 28 15:17:24 2008 +0200 +++ b/src/Pure/Isar/spec_parse.ML Sat Jun 28 15:17:26 2008 +0200 @@ -56,7 +56,7 @@ fun thm_name s = P.name -- opt_attribs --| P.$$$ s; fun opt_thm_name s = - Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []); + Scan.optional ((P.name -- opt_attribs || attribs >> pair "") --| P.$$$ s) ("", []); val spec = opt_thm_name ":" -- Scan.repeat1 P.prop; val named_spec = thm_name ":" -- Scan.repeat1 P.prop;