# HG changeset patch
# User wenzelm
# Date 921690101 -3600
# Node ID e6f0c192ef88b5783f4b13159fab9db641eb9eca
# Parent  e70ae9b575cc2bc33357e17836e3335f4f60fe80
fixed thm_name again;

diff -r e70ae9b575cc -r e6f0c192ef88 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Mar 17 17:20:36 1999 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Mar 17 18:01:41 1999 +0100
@@ -241,7 +241,7 @@
 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
 val opt_attribs = Scan.optional attribs [];
 
-fun thm_name s = name -- (!!! (opt_attribs --| $$$ s));
+fun thm_name s = name -- opt_attribs --| $$$ s;
 fun opt_thm_name s = Scan.optional (thm_name s) ("", []);
 
 val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));