src/Pure/Isar/parse_spec.ML

--- a/src/Pure/Isar/parse_spec.ML	Thu Aug 21 13:46:29 2014 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Thu Aug 21 22:48:39 2014 +0200
@@ -6,16 +6,12 @@
 
 signature PARSE_SPEC =
 sig
-  val attribs: Token.src list parser
-  val opt_attribs: Token.src list parser
   val thm_name: string -> Attrib.binding parser
   val opt_thm_name: string -> Attrib.binding parser
   val spec: (Attrib.binding * string) parser
   val specs: (Attrib.binding * string list) parser
   val alt_specs: (Attrib.binding * string) list parser
   val where_alt_specs: (Attrib.binding * string) list parser
-  val xthm: (Facts.ref * Token.src list) parser
-  val xthms1: (Facts.ref * Token.src list) list parser
   val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
   val constdecl: (binding * string option * mixfix) parser
   val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
@@ -37,14 +33,11 @@
 
 (* theorem specifications *)
 
-val attrib = Parse.position Parse.liberal_name -- Parse.!!! Parse.args >> uncurry Token.src;
-val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
-val opt_attribs = Scan.optional attribs [];
-
-fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
+fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s;
 
 fun opt_thm_name s =
-  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
+  Scan.optional
+    ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s)
     Attrib.empty_binding;
 
 val spec = opt_thm_name ":" -- Parse.prop;
@@ -56,14 +49,7 @@
 
 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
 
-val xthm =
-  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
-  (Parse.literal_fact >> Facts.Fact ||
-    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
-
-val xthms1 = Scan.repeat1 xthm;
-
-val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1);
 
 
 (* basic constant specifications *)
@@ -103,7 +89,7 @@
     >> Element.Assumes ||
   Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
     >> Element.Defines ||
-  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
+  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1))
     >> (curry Element.Notes "");
 
 fun plus1_unless test scan =