# HG changeset patch # User wenzelm # Date 1218314638 -7200 # Node ID 0dfed2f2822abcdf7885d1d509c06d7aab6bd2f9 # Parent 2d36632bc5de07bbc0934dbbbd5ecb71b6cbf357 unified Args.T with OuterLex.token, renamed some operations; moved thm_sel to attrib.ML; diff -r 2d36632bc5de -r 0dfed2f2822a src/Pure/Isar/spec_parse.ML --- a/src/Pure/Isar/spec_parse.ML Sat Aug 09 22:43:57 2008 +0200 +++ b/src/Pure/Isar/spec_parse.ML Sat Aug 09 22:43:58 2008 +0200 @@ -50,7 +50,7 @@ (* theorem specifications *) -val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src; +val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src; val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]"; val opt_attribs = Scan.optional attribs []; @@ -64,15 +64,10 @@ val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)); val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)); -val thm_sel = P.$$$ "(" |-- P.list1 - (P.nat --| P.minus -- P.nat >> Facts.FromTo || - P.nat --| P.minus >> Facts.From || - P.nat >> Facts.Single) --| P.$$$ ")"; - val xthm = P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") || (P.alt_string >> Facts.Fact || - P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs; + P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs; val xthms1 = Scan.repeat1 xthm;