# HG changeset patch # User wenzelm # Date 1392928034 -3600 # Node ID 00e900057b38673fd17d6deb99f75cbcf54816fe # Parent 306ff289da3a2a5b402147cb02fffafb91396546 tuned signature; tuned message; diff -r 306ff289da3a -r 00e900057b38 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu Feb 20 21:04:24 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Thu Feb 20 21:27:14 2014 +0100 @@ -1082,18 +1082,19 @@ (case term_of t0 of Abs (a, T, _) => let - val (b, ctxt') = Variable.next_bound (a, T) ctxt; - val (v, t') = Thm.dest_abs (SOME b) t0; - val b' = #1 (Term.dest_Free (term_of v)); + val (v, ctxt') = Variable.next_bound (a, T) ctxt; + val b = #1 (Term.dest_Free v); + val (v', t') = Thm.dest_abs (SOME b) t0; + val b' = #1 (Term.dest_Free (term_of v')); val _ = if b <> b' then - warning ("Simplifier: renamed bound variable " ^ + warning ("Bad Simplifier context: renamed bound variable " ^ quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ())) else (); val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0); in (case botc skel' ctxt' t' of - SOME thm => SOME (Thm.abstract_rule a v thm) + SOME thm => SOME (Thm.abstract_rule a v' thm) | NONE => NONE) end | t $ _ => diff -r 306ff289da3a -r 00e900057b38 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Feb 20 21:04:24 2014 +0100 +++ b/src/Pure/variable.ML Thu Feb 20 21:27:14 2014 +0100 @@ -32,7 +32,7 @@ val lookup_const: Proof.context -> string -> string option val is_const: Proof.context -> string -> bool val declare_const: string * string -> Proof.context -> Proof.context - val next_bound: string * typ -> Proof.context -> string * Proof.context + val next_bound: string * typ -> Proof.context -> term * Proof.context val revert_bounds: Proof.context -> term -> term val is_fixed: Proof.context -> string -> bool val newly_fixed: Proof.context -> Proof.context -> string -> bool @@ -313,7 +313,7 @@ let val b = Name.bound (#1 (#bounds (rep_data ctxt))); val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds)); - in (b, ctxt') end; + in (Free (b, T), ctxt') end; fun revert_bounds ctxt t = (case #2 (#bounds (rep_data ctxt)) of