# HG changeset patch
# User wenzelm
# Date 925202557 -7200
# Node ID 11b07125422e29746aa1c6a3eb62ef8e619a2e61
# Parent  b5ef6d115b45696b3e3b1a6bab8c9b19a4d7264b
opt_thm_name: name optional;

diff -r b5ef6d115b45 -r 11b07125422e src/Pure/Isar/outer_parse.ML
--- 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));