src/HOL/Tools/datatype_codegen.ML
changeset 22554 d1499fff65d8
parent 22480 b20bc8029edb
child 22566 535ae9dd4c45
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Mar 30 16:19:02 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Mar 30 16:19:03 2007 +0200
     1.3 @@ -620,11 +620,10 @@
     1.4      fun add_eq_thms (dtco, (_, (vs, cs))) thy =
     1.5        let
     1.6          val thy_ref = Theory.self_ref thy;
     1.7 -        val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
     1.8 -        val c = CodegenConsts.norm thy ("op =", [ty]);
     1.9 +        val const = ("op =", SOME dtco);
    1.10          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.11        in
    1.12 -        CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy
    1.13 +        CodegenData.add_funcl (const, CodegenData.lazy get_thms) thy
    1.14        end;
    1.15    in
    1.16      prove_codetypes_arities (ClassPackage.intro_classes_tac [])