src/Pure/Isar/attrib.ML
changeset 18037 1095d2213b9d
parent 17756 d4a35f82fbb4
child 18236 dd445f5cb28e
--- a/src/Pure/Isar/attrib.ML	Fri Oct 28 22:28:06 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Oct 28 22:28:07 2005 +0200
@@ -169,11 +169,15 @@
 (* theorems *)
 
 fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
-  Scan.ahead Args.name -- Args.named_fact (fn name => get st (Name name)) --
-  Scan.option Args.thm_sel -- Args.opt_attribs (intern (theory_of st))
-  >> (fn (((name, fact), sel), srcs) =>
+ (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
+    >> (fn (s, fact) => ("", Fact s, fact)) ||
+  Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel
+    >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
+  Scan.ahead Args.name -- Args.named_fact (get st o Name)
+    >> (fn (name, fact) => (name, Name name, fact))) --
+  Args.opt_attribs (intern (theory_of st))
+  >> (fn ((name, thmref, fact), srcs) =>
     let
-      val thmref = (case sel of NONE => Name name | SOME is => NameSelection (name, is));
       val ths = PureThy.select_thm thmref fact;
       val atts = map (attrib (theory_of st)) srcs;
       val (st', ths') = Thm.applys_attributes ((st, ths), atts);