--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed May 05 18:25:34 2010 +0200
@@ -306,11 +306,11 @@
map_node node_id (K (NONE, module',
string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
[str ";"])) ^ "\n\n" ^
- (if "term_of" mem !mode then
+ (if member (op =) (!mode) "term_of" then
string_of (Pretty.blk (0, separate Pretty.fbrk
(mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
else "") ^
- (if "test" mem !mode then
+ (if member (op =) (!mode) "test" then
string_of (Pretty.blk (0, separate Pretty.fbrk
(mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
else ""))) gr2