src/HOL/Library/ExecutableSet.thy
changeset 21191 c00161fbf990
parent 21153 8288c8f203de
child 21321 9022a90f6fdd
--- a/src/HOL/Library/ExecutableSet.thy	Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Nov 06 16:28:31 2006 +0100
@@ -235,10 +235,8 @@
 nonfix union;
 *}
 
-code_constname
-  "ExecutableSet.member" "List.member"
-  "ExecutableSet.insertl" "List.insertl"
-  "ExecutableSet.drop_first" "List.drop_first"
+code_modulename SML
+  ExecutableSet List
 
 definition [code inline]:
   "empty_list = []"
@@ -285,7 +283,7 @@
   Bex \<equiv> Blex
 
 code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  image Union Inter UNION INTER Ball Bex (SML *)
+  image Union Inter UNION INTER Ball Bex (SML -)
 
 
 subsection {* type serializations *}