# HG changeset patch
# User wenzelm
# Date 1185566123 -7200
# Node ID 3063a756611d0b9fe1e1d208f4e67e4931053861
# Parent  e48e1b4557c8f0c51168357d3bb789ebbba4491b
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);

diff -r e48e1b4557c8 -r 3063a756611d src/Pure/Isar/spec_parse.ML
--- 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);