src/HOL/Tools/datatype_codegen.ML
changeset 22480 b20bc8029edb
parent 22435 16e6ddc30f92
child 22554 d1499fff65d8
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Mar 20 10:23:31 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Mar 20 15:52:37 2007 +0100
     1.3 @@ -340,7 +340,7 @@
     1.4          val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
     1.5          val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
     1.6        in case t'
     1.7 -       of Const ("undefined", _) => NONE
     1.8 +       of Const ("HOL.undefined", _) => NONE
     1.9          | _ => SOME (c', t')
    1.10        end;
    1.11    in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts' |> map_filter I)) end;
    1.12 @@ -423,7 +423,7 @@
    1.13    let
    1.14      val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
    1.15    in
    1.16 -    fold_rev CodegenData.add_func case_rewrites thy
    1.17 +    fold_rev (CodegenData.add_func true) case_rewrites thy
    1.18    end;
    1.19  
    1.20