1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Apr 28 09:32:28 2011 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Apr 28 20:20:49 2011 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  sig
     1.5    val cert_def: Proof.context -> term -> (string * typ) * term
     1.6    val abs_def: term -> (string * typ) * term
     1.7 -  val mk_def: Proof.context -> (binding * term) list -> term list
     1.8    val expand: cterm list -> thm -> thm
     1.9    val def_export: Assumption.export
    1.10    val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
    1.11 @@ -57,9 +56,10 @@
    1.12  
    1.13  fun mk_def ctxt args =
    1.14    let
    1.15 -    val (xs, rhss) = split_list args;
    1.16 -    val (bind, _) = Proof_Context.bind_fixes xs ctxt;
    1.17 -    val lhss = map (fn (x, rhs) => bind (Free (Binding.name_of x, Term.fastype_of rhs))) args;
    1.18 +    val (bs, rhss) = split_list args;
    1.19 +    val Ts = map Term.fastype_of rhss;
    1.20 +    val (xs, _) = Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts) ctxt;
    1.21 +    val lhss = ListPair.map Free (xs, Ts);
    1.22    in map Logic.mk_equals (lhss ~~ rhss) end;
    1.23  
    1.24  

     2.1 --- a/src/Pure/Isar/obtain.ML	Thu Apr 28 09:32:28 2011 +0200
     2.2 +++ b/src/Pure/Isar/obtain.ML	Thu Apr 28 20:20:49 2011 +0200
     2.3 @@ -99,8 +99,9 @@
     2.4  
     2.5  fun bind_judgment ctxt name =
     2.6    let
     2.7 -    val (bind, ctxt') = Proof_Context.bind_fixes [Binding.name name] ctxt;
     2.8 -    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) name);
     2.9 +    val thy = Proof_Context.theory_of ctxt;
    2.10 +    val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
    2.11 +    val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
    2.12    in ((v, t), ctxt') end;
    2.13  
    2.14  val thatN = "that";
    2.15 @@ -278,9 +279,9 @@
    2.16        let
    2.17          val ((parms, rule), ctxt') =
    2.18            unify_params vars thesis_var raw_rule (Proof.context_of state');
    2.19 -        val (bind, _) = Proof_Context.bind_fixes (map (Binding.name o #1 o #1) parms) ctxt';
    2.20 -        val ts = map (bind o Free o #1) parms;
    2.21 -        val ps = map dest_Free ts;
    2.22 +        val (xs, _) = Variable.add_fixes (map (#1 o #1) parms) ctxt';
    2.23 +        val ps = xs ~~ map (#2 o #1) parms;
    2.24 +        val ts = map Free ps;
    2.25          val asms =
    2.26            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
    2.27            |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));

     3.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 28 09:32:28 2011 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 28 20:20:49 2011 +0200
     3.3 @@ -125,7 +125,6 @@
     3.4    val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
     3.5      string list * Proof.context
     3.6    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
     3.7 -  val bind_fixes: binding list -> Proof.context -> (term -> term) * Proof.context
     3.8    val add_assms: Assumption.export ->
     3.9      (Thm.binding * (string * string list) list) list ->
    3.10      Proof.context -> (string * thm list) list * Proof.context
    3.11 @@ -1038,25 +1037,9 @@
    3.12        #> pair xs)
    3.13    end;
    3.14  
    3.15 -
    3.16 -(* fixes vs. frees *)
    3.17 -
    3.18  fun auto_fixes (ctxt, (propss, x)) =
    3.19    ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
    3.20  
    3.21 -fun bind_fixes bs ctxt =
    3.22 -  let
    3.23 -    val (_, ctxt') = ctxt |> add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
    3.24 -    val xs = map Binding.name_of bs;
    3.25 -    fun bind (t as Free (x, T)) =
    3.26 -          if member (op =) xs x then
    3.27 -            (case Variable.lookup_fixed ctxt' x of SOME x' => Free (x', T) | NONE => t)
    3.28 -          else t
    3.29 -      | bind (t $ u) = bind t $ bind u
    3.30 -      | bind (Abs (x, T, t)) = Abs (x, T, bind t)
    3.31 -      | bind a = a;
    3.32 -  in (bind, ctxt') end;
    3.33 -
    3.34  
    3.35  
    3.36  (** assumptions **)
    3.37 @@ -1109,11 +1092,9 @@
    3.38      else error ("Illegal schematic variable(s) in case " ^ quote name)
    3.39    end;
    3.40  
    3.41 -fun fix (x, T) ctxt =
    3.42 -  let
    3.43 -    val (bind, ctxt') = bind_fixes [x] ctxt;
    3.44 -    val t = bind (Free (Binding.name_of x, T));
    3.45 -  in (t, ctxt' |> Variable.declare_constraints t) end;
    3.46 +fun fix (b, T) ctxt =
    3.47 +  let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
    3.48 +  in (Free (x, T), ctxt') end;
    3.49  
    3.50  in
    3.51