--- 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));