src/Pure/Isar/spec_parse.ML

 
 
 (* theorem specifications *)
 
 val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
-val attribs = P.$$$ "[" |-- P.!!! (P.list attrib --| P.$$$ "]");
+val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
 val opt_attribs = Scan.optional attribs [];
 
 fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
 fun opt_thm_name s =
   Scan.optional ((P.name -- opt_attribs || (attribs >> pair "")) --| P.$$$ s) ("", []);