src/HOL/Tools/datatype_codegen.ML
changeset 20439 1bf42b262a38
parent 20435 d2a30fed7596
child 20597 65fe827aa595
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 12:28:39 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 15:11:17 2006 +0200
     1.3 @@ -426,7 +426,7 @@
     1.4    let
     1.5      val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
     1.6    in
     1.7 -    CodegenPackage.add_appconst_i (case_name, CodegenPackage.appgen_case dest_case_expr) thy
     1.8 +    CodegenPackage.add_appconst (case_name, CodegenPackage.appgen_case dest_case_expr) thy
     1.9    end;
    1.10  
    1.11  fun add_datatype_case_defs dtco thy =