--- a/src/HOL/Algebra/abstract/Ring.thy Mon Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Mon Oct 17 23:10:15 2005 +0200
@@ -167,7 +167,7 @@
let val rew = Tactic.prove sg [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
- (fn _ => simp_tac (Simplifier.inherit_bounds ss ring_ss) 1)
+ (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
|> mk_meta_eq;
val (t', u) = Logic.dest_equals (Thm.prop_of rew);
in if t' aconv u