# HG changeset patch
# User haftmann
# Date 1255332326 -7200
# Node ID fbccf4522e147a78b1c383527f0bf4c56e9701b3
# Parent  5564af2d0588a46882f0a3d6a78c8a9c41b56947
using distinct rules directly

diff -r 5564af2d0588 -r fbccf4522e14 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Oct 09 13:40:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 12 09:25:26 2009 +0200
@@ -365,7 +365,8 @@
 fun mk_eq_eqns thy dtco =
   let
     val (vs, cos) = Datatype.the_spec thy dtco;
-    val { descr, index, inject = inject_thms, ... } = Datatype.the_info thy dtco;
+    val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
+      Datatype.the_info thy dtco;
     val ty = Type (dtco, map TFree vs);
     fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
       $ t1 $ t2;
@@ -381,9 +382,8 @@
       [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
     val distincts = maps prep_distinct (snd (nth (DatatypeProp.make_distincts [descr] vs) index));
     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
-    val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss
-      addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
-      addsimprocs [Datatype.distinct_simproc]);
+    val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
+      (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
     fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
   in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;