| changeset 16498 | 9d265401fee0 |
| parent 16169 | b59202511b8a |
| child 16736 | 1e792b32abef |
--- a/src/Pure/Isar/outer_parse.ML Mon Jun 20 22:14:11 2005 +0200 +++ b/src/Pure/Isar/outer_parse.ML Mon Jun 20 22:14:12 2005 +0200 @@ -305,7 +305,7 @@ nat --| minus >> PureThy.From || nat >> PureThy.Single) --| $$$ ")"; -val xthm = xname -- Scan.option thm_sel -- opt_attribs; +val xthm = (xname -- thm_sel >> NameSelection || xname >> Name) -- opt_attribs; val xthms1 = Scan.repeat1 xthm;