--- a/src/Pure/Isar/spec_parse.ML Thu Mar 20 12:09:22 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML Thu Mar 20 16:04:30 2008 +0100
@@ -70,8 +70,9 @@
P.nat >> Facts.Single) --| P.$$$ ")";
val xthm =
- P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
- (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
+ P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
+ (P.alt_string >> Facts.Fact ||
+ P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
val xthms1 = Scan.repeat1 xthm;