src/HOL/Tools/datatype_codegen.ML
changeset 21454 a1937c51ed88
parent 21046 fe1db2f991a7
child 21516 c2a116a2c4fd
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Nov 22 10:20:11 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Nov 22 10:20:12 2006 +0100
     1.3 @@ -489,7 +489,6 @@
     1.4    | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
     1.5  
     1.6  local
     1.7 -  val eq_def_sym = thm "eq_def" |> Thm.symmetric;
     1.8    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
     1.9     of SOME _ => get_eq_datatype thy tyco
    1.10      | NONE => [TypecopyPackage.get_eq thy tyco];
    1.11 @@ -498,7 +497,6 @@
    1.12      get_eq_thms thy tyco
    1.13      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy)
    1.14      |> HOL.constrain_op_eq_thms thy
    1.15 -    |> map (Tactic.rewrite_rule [eq_def_sym])
    1.16  end;
    1.17  
    1.18  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
    1.19 @@ -605,7 +603,7 @@
    1.20        let
    1.21          val thy_ref = Theory.self_ref thy;
    1.22          val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
    1.23 -        val c = CodegenConsts.norm thy ("Code_Generator.eq", [ty]);
    1.24 +        val c = CodegenConsts.norm thy ("op =", [ty]);
    1.25          val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.26        in
    1.27          CodegenData.add_funcl (c, CodegenData.lazy get_thms) thy