diff -r 839db6346cc8 -r f4b83f03cac9 src/HOL/ex/ReflectionEx.thy
--- a/src/HOL/ex/ReflectionEx.thy	Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/ex/ReflectionEx.thy	Sat Jun 23 19:33:22 2007 +0200
@@ -164,7 +164,7 @@
 lemma lin_add: "Inum bs (lin_add (t,s)) = Inum bs (Add t s)"
 apply (induct t s rule: lin_add.induct, simp_all add: Let_def)
 apply (case_tac "c1+c2 = 0",case_tac "n1 \<le> n2", simp_all)
-by (case_tac "n1 = n2", simp_all add: ring_eq_simps)
+by (case_tac "n1 = n2", simp_all add: ring_simps)
 
 consts lin_mul :: "num \<Rightarrow> nat \<Rightarrow> num"
 recdef lin_mul "measure size "
@@ -173,7 +173,7 @@
   "lin_mul t = (\<lambda> i. Mul i t)"
 
 lemma lin_mul: "Inum bs (lin_mul t i) = Inum bs (Mul i t)"
-by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_eq_simps)
+by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: ring_simps)
 
 consts linum:: "num \<Rightarrow> num"
 recdef linum "measure num_size"