# HG changeset patch
# User paulson
# Date 993567978 -7200
# Node ID cde6edd51ff6ba0997c43114d4b5a15ebe59f17a
# Parent  297625089e80a60498867d6f74e25726bde3ecee
resolved name clash

diff -r 297625089e80 -r cde6edd51ff6 src/HOL/Algebra/abstract/Ideal.ML
--- a/src/HOL/Algebra/abstract/Ideal.ML	Tue Jun 26 17:05:10 2001 +0200
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Tue Jun 26 17:06:18 2001 +0200
@@ -168,14 +168,14 @@
 by (rtac psubsetI 1);
 by (etac dvd_imp_subideal 1);
 by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); 
-qed "not_dvd_psubideal";
+qed "not_dvd_psubideal_singleton";
 
 Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)";
 by (rtac iffI 1);
 by (REPEAT (ares_tac
   [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
 by (etac conjE 1);
-by (REPEAT (ares_tac [not_dvd_psubideal] 1));
+by (REPEAT (ares_tac [not_dvd_psubideal_singleton] 1));
 qed "psubideal_is_dvd";
 
 Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}";