1.1 --- a/src/HOL/Library/Executable_Set.thy	Sun Jan 31 14:51:32 2010 +0100
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Sun Jan 31 19:07:03 2010 +0100
     1.3 @@ -93,14 +93,14 @@
     1.4    by simp
     1.5  
     1.6  lemma insert_Set [code]:
     1.7 -  "insert x (Set xs) = Set (List_Set.insert x xs)"
     1.8 -  "insert x (Coset xs) = Coset (remove_all x xs)"
     1.9 -  by (simp_all add: insert_set insert_set_compl)
    1.10 +  "insert x (Set xs) = Set (List.insert x xs)"
    1.11 +  "insert x (Coset xs) = Coset (removeAll x xs)"
    1.12 +  by (simp_all add: set_insert)
    1.13  
    1.14  lemma remove_Set [code]:
    1.15 -  "remove x (Set xs) = Set (remove_all x xs)"
    1.16 -  "remove x (Coset xs) = Coset (List_Set.insert x xs)"
    1.17 -  by (simp_all add:remove_set remove_set_compl)
    1.18 +  "remove x (Set xs) = Set (removeAll x xs)"
    1.19 +  "remove x (Coset xs) = Coset (List.insert x xs)"
    1.20 +  by (auto simp add: set_insert remove_def)
    1.21  
    1.22  lemma image_Set [code]:
    1.23    "image f (Set xs) = Set (remdups (map f xs))"