src/Pure/Isar/spec_parse.ML
changeset 26361 7946f459c6c8
parent 26336 a0e2b706ce73
child 27378 0968c0d0b969
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Thu Mar 20 12:09:22 2008 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Thu Mar 20 16:04:30 2008 +0100
     1.3 @@ -70,8 +70,9 @@
     1.4    P.nat >> Facts.Single) --| P.$$$ ")";
     1.5  
     1.6  val xthm =
     1.7 -  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.Named ("", NONE)) ||
     1.8 -  (P.alt_string >> Facts.Fact || P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
     1.9 +  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    1.10 +  (P.alt_string >> Facts.Fact ||
    1.11 +    P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
    1.12  
    1.13  val xthms1 = Scan.repeat1 xthm;
    1.14