eliminated slightly odd Proof_Context.bind_fixes;
tuned;

--- a/src/Pure/Isar/local_defs.ML	Thu Apr 28 09:32:28 2011 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Apr 28 20:20:49 2011 +0200
@@ -8,7 +8,6 @@
 sig
   val cert_def: Proof.context -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
-  val mk_def: Proof.context -> (binding * term) list -> term list
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
   val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
@@ -57,9 +56,10 @@
 
 fun mk_def ctxt args =
   let
-    val (xs, rhss) = split_list args;
-    val (bind, _) = Proof_Context.bind_fixes xs ctxt;
-    val lhss = map (fn (x, rhs) => bind (Free (Binding.name_of x, Term.fastype_of rhs))) args;
+    val (bs, rhss) = split_list args;
+    val Ts = map Term.fastype_of rhss;
+    val (xs, _) = Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts) ctxt;
+    val lhss = ListPair.map Free (xs, Ts);
   in map Logic.mk_equals (lhss ~~ rhss) end;
 
 

--- a/src/Pure/Isar/obtain.ML	Thu Apr 28 09:32:28 2011 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Apr 28 20:20:49 2011 +0200
@@ -99,8 +99,9 @@
 
 fun bind_judgment ctxt name =
   let
-    val (bind, ctxt') = Proof_Context.bind_fixes [Binding.name name] ctxt;
-    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
+    val thy = Proof_Context.theory_of ctxt;
+    val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
+    val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
   in ((v, t), ctxt') end;
 
 val thatN = "that";
@@ -278,9 +279,9 @@
       let
         val ((parms, rule), ctxt') =
           unify_params vars thesis_var raw_rule (Proof.context_of state');
-        val (bind, _) = Proof_Context.bind_fixes (map (Binding.name o #1 o #1) parms) ctxt';
-        val ts = map (bind o Free o #1) parms;
-        val ps = map dest_Free ts;
+        val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt';
+        val ps = xs ~~ map (#2 o #1) parms;
+        val ts = map Free ps;
         val asms =
           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
           |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));

--- a/src/Pure/Isar/proof_context.ML	Thu Apr 28 09:32:28 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 28 20:20:49 2011 +0200
@@ -125,7 +125,6 @@
   val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     string list * Proof.context
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
-  val bind_fixes: binding list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
@@ -1038,25 +1037,9 @@
       #> pair xs)
   end;
 
-
-(* fixes vs. frees *)
-
 fun auto_fixes (ctxt, (propss, x)) =
   ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
 
-fun bind_fixes bs ctxt =
-  let
-    val (_, ctxt') = ctxt |> add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
-    val xs = map Binding.name_of bs;
-    fun bind (t as Free (x, T)) =
-          if member (op =) xs x then
-            (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
-          else t
-      | bind (t $ u) = bind t $ bind u
-      | bind (Abs (x, T, t)) = Abs (x, T, bind t)
-      | bind a = a;
-  in (bind, ctxt') end;
-
 
 
 (** assumptions **)
@@ -1109,11 +1092,9 @@
     else error ("Illegal schematic variable(s) in case " ^ quote name)
   end;
 
-fun fix (x, T) ctxt =
-  let
-    val (bind, ctxt') = bind_fixes [x] ctxt;
-    val t = bind (Free (Binding.name_of x, T));
-  in (t, ctxt' |> Variable.declare_constraints t) end;
+fun fix (b, T) ctxt =
+  let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
+  in (Free (x, T), ctxt') end;
 
 in