# HG changeset patch
# User blanchet
# Date 1514901666 -3600
# Node ID 9301e197a47b38441fda88e1b8805061c9672ddb
# Parent  315b5c29e9270ec9f3b9d36ed519a9ed7896566f
removed needless theorems

diff -r 315b5c29e927 -r 9301e197a47b src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jan 02 14:42:00 2018 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Jan 02 15:01:06 2018 +0100
@@ -28,10 +28,6 @@
 val finite_Diff = @{thm finite_Diff};
 val finite_Un = @{thm finite_Un};
 val Un_iff = @{thm Un_iff};
-val In0_eq = @{thm In0_eq};
-val In1_eq = @{thm In1_eq};
-val In0_not_In1 = @{thm In0_not_In1};
-val In1_not_In0 = @{thm In1_not_In0};
 val Un_assoc = @{thm Un_assoc};
 val Collect_disj_eq = @{thm Collect_disj_eq};
 val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
@@ -850,9 +846,8 @@
     (* prove distinctness theorems *)
 
     val distinct_props = Old_Datatype_Prop.make_distincts descr';
-    val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
-      dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
-        constr_rep_thmss dist_lemmas;
+    val dist_rewrites = map2 (fn rep_thms => fn dist_lemma => dist_lemma :: rep_thms)
+      constr_rep_thmss dist_lemmas;
 
     fun prove_distinct_thms _ [] = []
       | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) =