src/HOL/Fun.thy
changeset 17877 67d5ab1cb0d8
parent 17589 58eeffd73be1
child 17956 369e2af8ee45
     1.1 --- a/src/HOL/Fun.thy	Mon Oct 17 23:10:13 2005 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Oct 17 23:10:15 2005 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4    val current_ss = simpset ()
     1.5    fun fun_upd_prover ss =
     1.6      rtac eq_reflection 1 THEN rtac ext 1 THEN
     1.7 -    simp_tac (Simplifier.inherit_bounds ss current_ss) 1
     1.8 +    simp_tac (Simplifier.inherit_context ss current_ss) 1
     1.9  in
    1.10    val fun_upd2_simproc =
    1.11      Simplifier.simproc (Theory.sign_of (the_context ()))