tuned signature;
authorwenzelm
Thu Feb 20 21:27:14 2014 +0100 (2014-02-20)
changeset 5563500e900057b38
parent 55634 306ff289da3a
child 55636 9d120886c50b
tuned signature;
tuned message;
src/Pure/raw_simplifier.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Feb 20 21:04:24 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Feb 20 21:27:14 2014 +0100
     1.3 @@ -1082,18 +1082,19 @@
     1.4            (case term_of t0 of
     1.5                Abs (a, T, _) =>
     1.6                  let
     1.7 -                    val (b, ctxt') = Variable.next_bound (a, T) ctxt;
     1.8 -                    val (v, t') = Thm.dest_abs (SOME b) t0;
     1.9 -                    val b' = #1 (Term.dest_Free (term_of v));
    1.10 +                    val (v, ctxt') = Variable.next_bound (a, T) ctxt;
    1.11 +                    val b = #1 (Term.dest_Free v);
    1.12 +                    val (v', t') = Thm.dest_abs (SOME b) t0;
    1.13 +                    val b' = #1 (Term.dest_Free (term_of v'));
    1.14                      val _ =
    1.15                        if b <> b' then
    1.16 -                        warning ("Simplifier: renamed bound variable " ^
    1.17 +                        warning ("Bad Simplifier context: renamed bound variable " ^
    1.18                            quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
    1.19                        else ();
    1.20                      val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
    1.21                  in
    1.22                    (case botc skel' ctxt' t' of
    1.23 -                    SOME thm => SOME (Thm.abstract_rule a v thm)
    1.24 +                    SOME thm => SOME (Thm.abstract_rule a v' thm)
    1.25                    | NONE => NONE)
    1.26                  end
    1.27              | t $ _ =>
     2.1 --- a/src/Pure/variable.ML	Thu Feb 20 21:04:24 2014 +0100
     2.2 +++ b/src/Pure/variable.ML	Thu Feb 20 21:27:14 2014 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4    val lookup_const: Proof.context -> string -> string option
     2.5    val is_const: Proof.context -> string -> bool
     2.6    val declare_const: string * string -> Proof.context -> Proof.context
     2.7 -  val next_bound: string * typ -> Proof.context -> string * Proof.context
     2.8 +  val next_bound: string * typ -> Proof.context -> term * Proof.context
     2.9    val revert_bounds: Proof.context -> term -> term
    2.10    val is_fixed: Proof.context -> string -> bool
    2.11    val newly_fixed: Proof.context -> Proof.context -> string -> bool
    2.12 @@ -313,7 +313,7 @@
    2.13    let
    2.14      val b = Name.bound (#1 (#bounds (rep_data ctxt)));
    2.15      val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds));
    2.16 -  in (b, ctxt') end;
    2.17 +  in (Free (b, T), ctxt') end;
    2.18  
    2.19  fun revert_bounds ctxt t =
    2.20    (case #2 (#bounds (rep_data ctxt)) of