src/HOL/Algebra/abstract/Ring.ML

--- a/src/HOL/Algebra/abstract/Ring.ML	Tue Oct 17 08:41:42 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML	Tue Oct 17 10:20:43 2000 +0200
@@ -308,10 +308,7 @@
 qed "l_integral";
 
 Goal "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
-by (etac contrapos 1);
-by (rtac l_integral 1);
-by (assume_tac 1);
-by (assume_tac 1);
+by (blast_tac (claset() addIs [l_integral]) 1); 
 qed "not_integral";
 
 Addsimps [not_integral];