# HG changeset patch
# User wenzelm
# Date 1185567589 -7200
# Node ID d3873741678d4efc92291c37e5f42767d11933c3
# Parent  3063a756611d0b9fe1e1d208f4e67e4931053861
attribs: not cut (!!!);

diff -r 3063a756611d -r d3873741678d src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Fri Jul 27 21:55:23 2007 +0200
+++ b/src/Pure/Isar/spec_parse.ML	Fri Jul 27 22:19:49 2007 +0200
@@ -52,7 +52,7 @@
 (* theorem specifications *)
 
 val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
-val attribs = P.$$$ "[" |-- P.!!! (P.list attrib --| P.$$$ "]");
+val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
 val opt_attribs = Scan.optional attribs [];
 
 fun thm_name s = P.name -- opt_attribs --| P.$$$ s;