--- 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