--- a/src/Pure/variable.ML Tue Nov 28 00:35:27 2006 +0100
+++ b/src/Pure/variable.ML Tue Nov 28 00:35:28 2006 +0100
@@ -17,6 +17,7 @@
val is_declared: Proof.context -> string -> bool
val is_fixed: Proof.context -> string -> bool
val newly_fixed: Proof.context -> Proof.context -> string -> bool
+ val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
val default_type: Proof.context -> string -> typ option
val def_type: Proof.context -> bool -> indexname -> typ option
val def_sort: Proof.context -> indexname -> sort option
@@ -126,6 +127,9 @@
fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
+fun add_fixed ctxt = Term.fold_aterms
+ (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);
+
(** declarations **)