src/HOL/Algebra/Ideal.thy

--- a/src/HOL/Algebra/Ideal.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Algebra/Ideal.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -787,7 +787,7 @@
       abI: "a \<otimes> b \<in> I" and
       anI: "a \<notin> I" and
       bnI: "b \<notin> I" by fast
-    def J \<equiv> "{x\<in>carrier R. a \<otimes> x \<in> I}"
+    define J where "J = {x\<in>carrier R. a \<otimes> x \<in> I}"
     
     from is_cring and acarr have idealJ: "ideal J R"
       unfolding J_def by (rule helper_max_prime)