| changeset 40793 | d21aedaa91e7 |
| parent 36955 | 226fb165833e |
| child 40800 | 330eb65c9469 |
--- a/src/Pure/Isar/parse_spec.ML Sun Nov 28 19:35:14 2010 +0100 +++ b/src/Pure/Isar/parse_spec.ML Sun Nov 28 20:03:19 2010 +0100 @@ -61,7 +61,7 @@ val xthm = Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") || - (Parse.alt_string >> Facts.Fact || + (Parse.literal_fact >> Facts.Fact || Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs; val xthms1 = Scan.repeat1 xthm;