# HG changeset patch
# User berghofe
# Date 1263143460 -3600
# Node ID 771830d3bd5e1107b4ab96218b74337c267c9ed9
# Parent  b23bd3ee4813319e7fc289664cb1a445a249039b
Injectivity / distinctness theorems are now used to simplify induction rules.

diff -r b23bd3ee4813 -r 771830d3bd5e src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Sun Jan 10 18:09:11 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sun Jan 10 18:11:00 2010 +0100
@@ -341,7 +341,8 @@
         ((Binding.empty, flat inject), [iff_add]),
         ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
           [Classical.safe_elim NONE]),
-        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
+        ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
+        ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
         @ named_rules @ unnamed_rules)
     |> snd
     |> add_case_tr' case_names