src/HOL/Tools/datatype_codegen.ML
changeset 21708 45e7491bea47
parent 21565 bd28361f4c5b
child 21924 fe474e69e603
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Dec 07 21:44:13 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Dec 07 23:16:55 2006 +0100
     1.3 @@ -375,7 +375,7 @@
     1.4    in map mk_dist (sym_product cos) end;
     1.5  
     1.6  local
     1.7 -  val bool_eq_implies = thm "iffD1";
     1.8 +  val bool_eq_implies = iffD1;
     1.9    val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    1.10    val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
    1.11    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    1.12 @@ -387,7 +387,7 @@
    1.13      val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    1.14      val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    1.15        |> map (fn thm => bool_eq_implies OF [thm] )
    1.16 -      |> map (Tactic.rewrite_rule [rew_eq, rew_conj]);
    1.17 +      |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
    1.18      val ctxt = ProofContext.init thy;
    1.19      val simpset = Simplifier.context ctxt
    1.20        (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);