diff -r 2b4c09941e04 -r 2202a5648897 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Jun 14 12:13:12 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Jun 14 12:14:13 2006 +0200
@@ -234,7 +234,7 @@
 and gen_set aG i = gen_set' aG i i;
 *}
 
-code_syntax_tyco set
+code_typapp set
   ml ("_ list")
   haskell (target_atom "[_]")
 
@@ -261,7 +261,11 @@
   "ExecutableSet.insertl" "List.insertl"
   "ExecutableSet.drop_first" "List.drop_first"
 
-code_syntax_const
+code_generate (ml, haskell) 
+  insertl unionl intersect flip subtract map_distinct
+  unions intersects map_union map_inter Blall Blex
+
+code_constapp
   "{}"
     ml (target_atom "[]")
     haskell (target_atom "[]")