--- a/src/HOL/Algebra/RingHom.thy Thu Jun 21 17:28:53 2007 +0200
+++ b/src/HOL/Algebra/RingHom.thy Thu Jun 21 20:07:26 2007 +0200
@@ -8,7 +8,6 @@
imports Ideal
begin
-
section {* Homomorphisms of Non-Commutative Rings *}
text {* Lifting existing lemmas in a @{text ring_hom_ring} locale *}
@@ -67,7 +66,7 @@
assumes compatible_mult: "!!x y. [| x : carrier R; y : carrier R |] ==> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y"
and compatible_one: "h \<one> = \<one>\<^bsub>S\<^esub>"
shows "ring_hom_ring R S h"
-apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, assumption+)
+apply (intro ring_hom_ring.intro ring_hom_ring_axioms.intro, rule R.is_ring, rule S.is_ring)
apply (insert group_hom.homh[OF a_group_hom])
apply (unfold hom_def ring_hom_def, simp)
apply safe