src/Pure/Isar/outer_parse.ML

 val attrib = position (xname -- !!! (args false)) >> Args.src;
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];
 
 fun thm_name s = name -- opt_attribs --| $$$ s;
-fun opt_thm_name s = Scan.optional (thm_name s) ("", []);
+fun opt_thm_name s =
+  Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);;
 
 val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
 val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
 
 val xthm = xname -- opt_attribs;