diff -r 9953ff53cc64 -r bc2563c37b1a src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Thu Jun 21 17:28:53 2007 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Thu Jun 21 20:07:26 2007 +0200
@@ -542,7 +542,7 @@
   assumes icarr: "i \<in> carrier R"
   shows "principalideal (PIdl i) R"
 apply (rule principalidealI)
-apply (rule cgenideal_ideal, assumption)
+apply (rule cgenideal_ideal [OF icarr])
 proof -
   from icarr
       have "PIdl i = Idl {i}" by (rule cgenideal_eq_genideal)
@@ -559,7 +559,7 @@
   shows "Idl (I \<union> J) = I <+> J"
 apply rule
  apply (rule ring.genideal_minimal)
-   apply assumption
+   apply (rule R.is_ring)
   apply (rule add_ideals[OF idealI idealJ])
  apply (rule)
  apply (simp add: set_add_defs) apply (elim disjE) defer 1 defer 1
@@ -675,8 +675,11 @@
      and "\<forall>a. a \<in> carrier R \<longrightarrow> (\<forall>b. a \<otimes> b \<in> I \<longrightarrow> b \<in> carrier R \<longrightarrow> a \<in> I \<or> b \<in> I)"
   hence I_prime: "\<And> a b. \<lbrakk>a \<in> carrier R; b \<in> carrier R; a \<otimes> b \<in> I\<rbrakk> \<Longrightarrow> a \<in> I \<or> b \<in> I" by simp
   have "primeideal I R"
-      apply (rule primeideal.intro, assumption+)
-      by (rule primeideal_axioms.intro, rule InR, erule I_prime)
+      apply (rule primeideal.intro [OF is_ideal is_cring])
+      apply (rule primeideal_axioms.intro)
+       apply (rule InR)
+      apply (erule (2) I_prime)
+      done
   from this and notprime
       show "False" by simp
 qed
@@ -692,7 +695,7 @@
 lemma (in cring) zeroprimeideal_domainI:
   assumes pi: "primeideal {\<zero>} R"
   shows "domain R"
-apply (rule domain.intro, assumption+)
+apply (rule domain.intro, rule is_cring)
 apply (rule domain_axioms.intro)
 proof (rule ccontr, simp)
   interpret primeideal ["{\<zero>}" "R"] by (rule pi)
@@ -779,7 +782,8 @@
   shows "primeideal I R"
 apply (rule ccontr)
 apply (rule primeidealCE)
-  apply assumption+
+   apply (rule is_cring)
+  apply assumption
  apply (simp add: I_notcarr)
 proof -
   assume "\<exists>a b. a \<in> carrier R \<and> b \<in> carrier R \<and> a \<otimes> b \<in> I \<and> a \<notin> I \<and> b \<notin> I"