equal
deleted
inserted
replaced
52 val typ_abbrev: typ context_parser |
52 val typ_abbrev: typ context_parser |
53 val typ: typ context_parser |
53 val typ: typ context_parser |
54 val term: term context_parser |
54 val term: term context_parser |
55 val term_abbrev: term context_parser |
55 val term_abbrev: term context_parser |
56 val prop: term context_parser |
56 val prop: term context_parser |
57 val tyname: string context_parser |
57 val type_name: bool -> string context_parser |
58 val const: string context_parser |
58 val const: string context_parser |
59 val const_proper: string context_parser |
59 val const_proper: string context_parser |
60 val bang_facts: thm list context_parser |
60 val bang_facts: thm list context_parser |
61 val goal_spec: ((int -> tactic) -> tactic) context_parser |
61 val goal_spec: ((int -> tactic) -> tactic) context_parser |
62 val parse: token list parser |
62 val parse: token list parser |
207 val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of); |
207 val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of); |
208 |
208 |
209 |
209 |
210 (* type and constant names *) |
210 (* type and constant names *) |
211 |
211 |
212 val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of) |
212 fun type_name strict = |
|
213 Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict)) |
213 >> (fn Type (c, _) => c | TFree (a, _) => a | _ => ""); |
214 >> (fn Type (c, _) => c | TFree (a, _) => a | _ => ""); |
214 |
215 |
215 val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of) |
216 val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of) |
216 >> (fn Const (c, _) => c | Free (x, _) => x | _ => ""); |
217 >> (fn Const (c, _) => c | Free (x, _) => x | _ => ""); |
217 |
218 |