xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);

--- a/src/Pure/Isar/spec_parse.ML	Fri Jul 27 21:55:22 2007 +0200
+++ b/src/Pure/Isar/spec_parse.ML	Fri Jul 27 21:55:23 2007 +0200
@@ -70,8 +70,10 @@
   P.nat --| P.minus >> PureThy.From ||
   P.nat >> PureThy.Single) --| P.$$$ ")";
 
-val xthm = (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name)
-  -- opt_attribs;
+val xthm =
+  P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Name "") ||
+  (P.alt_string >> Fact || P.xname -- thm_sel >> NameSelection || P.xname >> Name) -- opt_attribs;
+
 val xthms1 = Scan.repeat1 xthm;
 
 val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);