diff -r 0035be079bee -r ead82c82da9e src/HOL/ex/Commutative_Ring_Complete.thy
--- a/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/ex/Commutative_Ring_Complete.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -150,7 +150,7 @@
     then obtain d where X:"x=Suc (Suc d)" ..
     from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
-    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
+    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
     with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   ultimately show ?case by blast
 next
@@ -168,7 +168,7 @@
     then obtain d where X:"x=Suc (Suc d)" ..
     from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
     with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
-    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp
+    with prems NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" "isnorm (PX Q2 y R)" by simp assumption
     with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
   ultimately show ?case by blast
 next