# HG changeset patch # User wenzelm # Date 1304014849 -7200 # Node ID 2b8c34f53388888c2b6843b2f6f666c797bea4b0 # Parent b99cc6f7df6354cea0750405937e4e5945349f94 eliminated slightly odd Proof_Context.bind_fixes; tuned; diff -r b99cc6f7df63 -r 2b8c34f53388 src/Pure/Isar/local_defs.ML --- 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; diff -r b99cc6f7df63 -r 2b8c34f53388 src/Pure/Isar/obtain.ML --- 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), [])); diff -r b99cc6f7df63 -r 2b8c34f53388 src/Pure/Isar/proof_context.ML --- 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