diff -r cd956c4eadff -r 7946f459c6c8 src/Pure/Isar/spec_parse.ML
--- 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;