Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thm parsers: include Args.internal_fact;
authorwenzelm
Thu, 06 Jul 2006 17:47:33 +0200
changeset 20029 16957e34cfab
parent 20028 b9752164ad92
child 20030 e62913ef9d24
thm parsers: include Args.internal_fact;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- 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)) ||
isabelle