# 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 "" || Args.name; + fun gen_thm pick = Scan.depend (fn st => - (Args.internal_fact - >> (fn 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) =>