src/Pure/Isar/attrib.ML
changeset 18037 1095d2213b9d
parent 17756 d4a35f82fbb4
child 18236 dd445f5cb28e
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Oct 28 22:28:06 2005 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Oct 28 22:28:07 2005 +0200
     1.3 @@ -169,11 +169,15 @@
     1.4  (* theorems *)
     1.5  
     1.6  fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
     1.7 -  Scan.ahead Args.name -- Args.named_fact (fn name => get st (Name name)) --
     1.8 -  Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
     1.9 -  >> (fn (((name, fact), sel), srcs) =>
    1.10 + (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
    1.11 +    >> (fn (s, fact) => ("", Fact s, fact)) ||
    1.12 +  Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel
    1.13 +    >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
    1.14 +  Scan.ahead Args.name -- Args.named_fact (get st o Name)
    1.15 +    >> (fn (name, fact) => (name, Name name, fact))) --
    1.16 +  Args.opt_attribs (intern (theory_of st))
    1.17 +  >> (fn ((name, thmref, fact), srcs) =>
    1.18      let
    1.19 -      val thmref = (case sel of NONE => Name name | SOME is => NameSelection (name, is));
    1.20        val ths = PureThy.select_thm thmref fact;
    1.21        val atts = map (attrib (theory_of st)) srcs;
    1.22        val (st', ths') = Thm.applys_attributes ((st, ths), atts);