src/HOL/Set.thy

--- a/src/HOL/Set.thy	Thu Sep 29 12:33:26 2005 +0200
+++ b/src/HOL/Set.thy	Thu Sep 29 12:43:40 2005 +0200
@@ -1175,7 +1175,8 @@
 lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
   by blast
 
-lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard]
+lemmas empty_not_insert = insert_not_empty [symmetric, standard]
+declare empty_not_insert [simp]
 
 lemma insert_absorb: "a \<in> A ==> insert a A = A"
   -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}