# HG changeset patch
# User wenzelm
# Date 1213024030 -7200
# Node ID d4145c286bd1425e2532f4e2ed489ff1a3ea42ca
# Parent  c1c27955d7ddd91cc798d02dfab7302ee6e72fd7
qualified DatatypePackage.distinct_simproc;

diff -r c1c27955d7dd -r d4145c286bd1 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Jun 09 17:07:08 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Jun 09 17:07:10 2008 +0200
@@ -416,7 +416,7 @@
     val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
     val ctxt = ProofContext.init thy;
     val simpset = Simplifier.context ctxt
-      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
     val cos = map (fn (co, tys) =>
         (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
     val tac = ALLGOALS (simp_tac simpset)