equal
deleted
inserted
replaced
15 val binds_of: Proof.context -> (typ * term) Vartab.table |
15 val binds_of: Proof.context -> (typ * term) Vartab.table |
16 val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table |
16 val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table |
17 val is_declared: Proof.context -> string -> bool |
17 val is_declared: Proof.context -> string -> bool |
18 val is_fixed: Proof.context -> string -> bool |
18 val is_fixed: Proof.context -> string -> bool |
19 val newly_fixed: Proof.context -> Proof.context -> string -> bool |
19 val newly_fixed: Proof.context -> Proof.context -> string -> bool |
|
20 val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list |
20 val default_type: Proof.context -> string -> typ option |
21 val default_type: Proof.context -> string -> typ option |
21 val def_type: Proof.context -> bool -> indexname -> typ option |
22 val def_type: Proof.context -> bool -> indexname -> typ option |
22 val def_sort: Proof.context -> indexname -> sort option |
23 val def_sort: Proof.context -> indexname -> sort option |
23 val declare_constraints: term -> Proof.context -> Proof.context |
24 val declare_constraints: term -> Proof.context -> Proof.context |
24 val declare_internal: term -> Proof.context -> Proof.context |
25 val declare_internal: term -> Proof.context -> Proof.context |
124 |
125 |
125 val is_declared = Name.is_declared o names_of; |
126 val is_declared = Name.is_declared o names_of; |
126 fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt); |
127 fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt); |
127 fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x); |
128 fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x); |
128 |
129 |
|
130 fun add_fixed ctxt = Term.fold_aterms |
|
131 (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I); |
|
132 |
129 |
133 |
130 |
134 |
131 (** declarations **) |
135 (** declarations **) |
132 |
136 |
133 (* default sorts and types *) |
137 (* default sorts and types *) |