src/HOL/Tools/datatype_codegen.ML
changeset 22566 535ae9dd4c45
parent 22554 d1499fff65d8
child 22578 b0eb5652f210
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Apr 03 17:05:52 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Apr 03 19:24:10 2007 +0200
     1.3 @@ -623,7 +623,7 @@
     1.4          val const = ("op =", SOME dtco);
     1.5          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
     1.6        in
     1.7 -        CodegenData.add_funcl (const, CodegenData.lazy get_thms) thy
     1.8 +        CodegenData.add_funcl (const, CodegenData.lazy_thms get_thms) thy
     1.9        end;
    1.10    in
    1.11      prove_codetypes_arities (ClassPackage.intro_classes_tac [])