# HG changeset patch
# User wenzelm
# Date 1164670528 -3600
# Node ID 6096c956a11fb6ab2f64ac47eb62926966648e20
# Parent  f20f9304ab4822fc7d4436c15029f89639af8c5a
added add_fixed;

diff -r f20f9304ab48 -r 6096c956a11f src/Pure/variable.ML
--- 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 **)