src/Pure/Isar/spec_parse.ML
changeset 27816 0dfed2f2822a
parent 27378 0968c0d0b969
child 28083 103d9282a946
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Sat Aug 09 22:43:57 2008 +0200
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Sat Aug 09 22:43:58 2008 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  (* theorem specifications *)
     1.6  
     1.7 -val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
     1.8 +val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
     1.9  val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
    1.10  val opt_attribs = Scan.optional attribs [];
    1.11  
    1.12 @@ -64,15 +64,10 @@
    1.13  val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    1.14  val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    1.15  
    1.16 -val thm_sel = P.$$$ "(" |-- P.list1
    1.17 - (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
    1.18 -  P.nat --| P.minus >> Facts.From ||
    1.19 -  P.nat >> Facts.Single) --| P.$$$ ")";
    1.20 -
    1.21  val xthm =
    1.22    P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    1.23    (P.alt_string >> Facts.Fact ||
    1.24 -    P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
    1.25 +    P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    1.26  
    1.27  val xthms1 = Scan.repeat1 xthm;
    1.28