src/HOL/Library/Executable_Set.thy

--- a/src/HOL/Library/Executable_Set.thy	Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Thu Mar 05 08:23:11 2009 +0100
@@ -178,7 +178,7 @@
 
 lemma iso_insert:
   "set (insertl x xs) = insert x (set xs)"
-  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
+  unfolding insertl_def iso_member by (simp add: insert_absorb)
 
 lemma iso_remove1:
   assumes distnct: "distinct xs"
@@ -261,7 +261,7 @@
 subsubsection {* const serializations *}
 
 consts_code
-  "{}" ("{*[]*}")
+  "Set.empty" ("{*[]*}")
   insert ("{*insertl*}")
   is_empty ("{*null*}")
   "op \<union>" ("{*unionl*}")