# HG changeset patch
# User nipkow
# Date 1034927598 -7200
# Node ID b0d8bad27f429256bf48bf97e8a196f2dbc94ce2
# Parent  ef123b9e80896ac9a11a3435febfacba5acf6e7b
Mod due to: Added a few thms about UN/INT/{}/UNIV

diff -r ef123b9e8089 -r b0d8bad27f42 src/HOL/Algebra/abstract/Ideal.ML
--- a/src/HOL/Algebra/abstract/Ideal.ML	Fri Oct 18 09:53:02 2002 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Fri Oct 18 09:53:18 2002 +0200
@@ -74,7 +74,7 @@
 qed "generator_in_ideal";
 
 Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV";
-by (auto_tac (claset() addSDs [is_ideal_mult], simpset()));
+by (force_tac (claset() addDs [is_ideal_mult], simpset()) 1);
   (* loops if is_ideal_mult is added as non-safe rule *)
 qed "ideal_of_one_eq";