src/HOL/Algebra/abstract/Ideal2.ML

 qed "ideal_of_mono";
 
 Goal "ideal_of {0::'a::ring} = {0}";
 by (simp_tac (simpset() addsimps [pideal_structure]) 1);
 by (rtac subset_antisym 1);
-by (auto_tac (claset() addIs [dvd_zero_left], simpset()));
+by (auto_tac (claset() addIs [thm "dvd_zero_left"], simpset()));
 qed "ideal_of_zero_eq";
 
 Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I";
 by (auto_tac (claset(),
   simpset() addsimps [pideal_structure, is_ideal_dvd]));

 qed "is_pidealD";
 
 (* Ideals and divisibility *)
 
 Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}";
-by (auto_tac (claset() addIs [dvd_trans_ring],
+by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
   simpset() addsimps [pideal_structure]));
 qed "dvd_imp_subideal";
 
 Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a";
 by (auto_tac (claset() addSDs [subsetD],

 
 Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b";
 by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
 by (etac conjE 1);
 by (dres_inst_tac [("c", "a")] subsetD 1);
-by (auto_tac (claset() addIs [dvd_trans_ring],
+by (auto_tac (claset() addIs [thm "dvd_trans_ring"],
   simpset()));
 qed "psubideal_not_dvd";
 
 Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
 by (rtac psubsetI 1);