144 local |
144 local |
145 |
145 |
146 val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms; |
146 val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms; |
147 |
147 |
148 fun gen_thm pick = Scan.depend (fn st => |
148 fun gen_thm pick = Scan.depend (fn st => |
149 (Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact) |
149 (Args.internal_fact |
|
150 >> (fn fact => ("<fact>", Name "", fact)) || |
|
151 Scan.ahead Args.alt_name -- Args.named_fact (get_thms st o Fact) |
150 >> (fn (s, fact) => ("", Fact s, fact)) || |
152 >> (fn (s, fact) => ("", Fact s, fact)) || |
151 Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel |
153 Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) -- Args.thm_sel |
152 >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) || |
154 >> (fn ((name, fact), sel) => (name, NameSelection (name, sel), fact)) || |
153 Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) |
155 Scan.ahead Args.name -- Args.named_fact (get_thms st o Name) |
154 >> (fn (name, fact) => (name, Name name, fact))) -- |
156 >> (fn (name, fact) => (name, Name name, fact))) -- |