src/HOL/Fun.thy
changeset 16973 b2a894562b8f
parent 16733 236dfafbeb63
child 17084 fb0a80aef0be
     1.1 --- a/src/HOL/Fun.thy	Mon Aug 01 19:20:25 2005 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Aug 01 19:20:26 2005 +0200
     1.3 @@ -486,15 +486,18 @@
     1.4          | find t = NONE
     1.5      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
     1.6  
     1.7 -  val ss = simpset ()
     1.8 -  val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1)
     1.9 +  val current_ss = simpset ()
    1.10 +  fun fun_upd_prover ss =
    1.11 +    rtac eq_reflection 1 THEN rtac ext 1 THEN
    1.12 +    simp_tac (Simplifier.inherit_bounds ss current_ss) 1
    1.13  in
    1.14    val fun_upd2_simproc =
    1.15      Simplifier.simproc (Theory.sign_of (the_context ()))
    1.16        "fun_upd2" ["f(v := w, x := y)"]
    1.17 -      (fn sg => fn _ => fn t =>
    1.18 +      (fn sg => fn ss => fn t =>
    1.19          case find_double t of (T, NONE) => NONE
    1.20 -        | (T, SOME rhs) => SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
    1.21 +        | (T, SOME rhs) =>
    1.22 +            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
    1.23  end;
    1.24  Addsimprocs[fun_upd2_simproc];
    1.25