diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeCollections.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -402,16 +402,16 @@
   "test1 = sum [None, Some True, None, Some False]"
   "test2 = (inf :: nat \<times> unit)"
 
-code_generate eq
-code_generate "op <<="
-code_generate "op <<"
-code_generate inf
-code_generate between
-code_generate index
-code_generate sum
-code_generate test1
-code_generate test2
+code_gen eq
+code_gen "op <<="
+code_gen "op <<"
+code_gen inf
+code_gen between
+code_gen index
+code_gen sum
+code_gen test1
+code_gen test2
 
-code_serialize ml (-)
+code_gen (SML -)
 
 end
\ No newline at end of file