src/Pure/variable.ML
changeset 21571 6096c956a11f
parent 21522 bd641d927437
child 21683 b90fa6c8e062
     1.1 --- a/src/Pure/variable.ML	Tue Nov 28 00:35:27 2006 +0100
     1.2 +++ b/src/Pure/variable.ML	Tue Nov 28 00:35:28 2006 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4    val is_declared: Proof.context -> string -> bool
     1.5    val is_fixed: Proof.context -> string -> bool
     1.6    val newly_fixed: Proof.context -> Proof.context -> string -> bool
     1.7 +  val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
     1.8    val default_type: Proof.context -> string -> typ option
     1.9    val def_type: Proof.context -> bool -> indexname -> typ option
    1.10    val def_sort: Proof.context -> indexname -> sort option
    1.11 @@ -126,6 +127,9 @@
    1.12  fun is_fixed ctxt x = exists (fn (_, y) => x = y) (fixes_of ctxt);
    1.13  fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
    1.14  
    1.15 +fun add_fixed ctxt = Term.fold_aterms
    1.16 +  (fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);
    1.17 +
    1.18  
    1.19  
    1.20  (** declarations **)