opt_thm_name: name optional;

--- a/src/Pure/Isar/outer_parse.ML	Tue Apr 27 10:42:08 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue Apr 27 10:42:37 1999 +0200
@@ -244,7 +244,8 @@
 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));