Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Fun.thy
changeset 17877 67d5ab1cb0d8
parent 17589 58eeffd73be1
child 17956 369e2af8ee45 
--- a/src/HOL/Fun.thy	Mon Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/Fun.thy	Mon Oct 17 23:10:15 2005 +0200
@@ -489,7 +489,7 @@
   val current_ss = simpset ()
   fun fun_upd_prover ss =
     rtac eq_reflection 1 THEN rtac ext 1 THEN
-    simp_tac (Simplifier.inherit_bounds ss current_ss) 1
+    simp_tac (Simplifier.inherit_context ss current_ss) 1
 in
   val fun_upd2_simproc =
     Simplifier.simproc (Theory.sign_of (the_context ()))
isabelle