# HG changeset patch
# User wenzelm
# Date 1152200853 -7200
# Node ID 16957e34cfaba5f53d95e8515b4d4237743e0609
# Parent  b9752164ad92440ed17148822901019a8d7c8250
thm parsers: include Args.internal_fact;

diff -r b9752164ad92 -r 16957e34cfab src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jul 06 16:49:40 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jul 06 17:47:33 2006 +0200
@@ -146,7 +146,9 @@
 val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
 
 fun gen_thm pick = Scan.depend (fn st =>
- (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact)
+ (Args.internal_fact
+    >> (fn fact => ("<fact>", Name "", 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
     >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) ||