# HG changeset patch
# User wenzelm
# Date 1165510729 -3600
# Node ID 43a842769765f3117ceabb1584e7ca4a6bef8f47
# Parent  49da72cad42d711068cb89d570f9d97323efdc82
thms etc.: proper treatment of internal_fact with selection;

diff -r 49da72cad42d -r 43a842769765 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Dec 07 17:58:48 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Dec 07 17:58:49 2006 +0100
@@ -155,14 +155,14 @@
 
 val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
 
+val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
+
 fun gen_thm pick = Scan.depend (fn st =>
- (Args.internal_fact
-    >> (fn fact => ("<fact>", Name "", fact)) ||
-  Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
+ (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
     >> (fn (s, fact) => ("", Fact s, fact)) ||
-  Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
+  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel
     >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||
-  Scan.ahead Args.name -- Args.named_fact (get_thms st o Name)
+  Scan.ahead fact_name -- Args.named_fact (get_thms st o Name)
     >> (fn (name, fact) => (name, Name name, fact))) --
   Args.opt_attribs (intern (Context.theory_of st))
   >> (fn ((name, thmref, fact), srcs) =>