src/HOL/Tools/typedef_codegen.ML
changeset 36692 54b64d4ad524
parent 35994 9cc3df9a606e
     1.1 --- a/src/HOL/Tools/typedef_codegen.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/typedef_codegen.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4                        Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
     1.5                          Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
     1.6                          Codegen.str "x) = x;"]) ^ "\n\n" ^
     1.7 -                      (if "term_of" mem !Codegen.mode then
     1.8 +                      (if member (op =) (!Codegen.mode) "term_of" then
     1.9                          Codegen.string_of (Pretty.block [Codegen.str "fun ",
    1.10                            Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    1.11                            Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    1.12 @@ -89,7 +89,7 @@
    1.13                            Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    1.14                            Codegen.str "x;"]) ^ "\n\n"
    1.15                         else "") ^
    1.16 -                      (if "test" mem !Codegen.mode then
    1.17 +                      (if member (op =) (!Codegen.mode) "test" then
    1.18                          Codegen.string_of (Pretty.block [Codegen.str "fun ",
    1.19                            Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    1.20                            Codegen.str "i =", Pretty.brk 1,