# 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