src/HOL/Tools/datatype_codegen.ML
changeset 19008 14c1b2f5dda4
parent 18963 3adfc9dfb30a
child 19346 c4c003abd830
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Feb 10 02:22:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Feb 10 09:09:07 2006 +0100
     1.3 @@ -297,13 +297,17 @@
     1.4    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
     1.5  
     1.6  
     1.7 -val setup =
     1.8 +val setup = 
     1.9    add_codegen "datatype" datatype_codegen #>
    1.10    add_tycodegen "datatype" datatype_tycodegen #>
    1.11    CodegenPackage.set_get_datatype
    1.12      DatatypePackage.get_datatype #>
    1.13    CodegenPackage.set_get_all_datatype_cons
    1.14      DatatypePackage.get_all_datatype_cons #>
    1.15 +  (fn thy => thy |> CodegenPackage.add_eqextr_default ("equality",
    1.16 +    (CodegenPackage.eqextr_eq
    1.17 +      DatatypePackage.get_eq_equations
    1.18 +      (Sign.read_term thy "False")))) #>
    1.19    CodegenPackage.ensure_datatype_case_consts
    1.20      DatatypePackage.get_datatype_case_consts
    1.21      DatatypePackage.get_case_const_data;