src/HOL/Tools/Datatype/datatype.ML

 fun stripC (i, f $ x) = stripC (i + 1, f)
   | stripC p = p;
 
 val distinctN = "constr_distinct";
 
-fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
-    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
-      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
-        atac 2, resolve_tac thms 1, etac FalseE 1]))
-  | ManyConstrs (thm, simpset) =>
-      let
-        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
-          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
-            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
-      in
-        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
-        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
-          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
-          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
-          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
-          etac FalseE 1]))
-      end;
+fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t
+  (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
+    atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1]));
 
 fun get_constr thy dtco =
   get_info thy dtco
   |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index);
 

       ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
       ||> Sign.restore_naming thy1;
   in
     thy2
     |> derive_datatype_props config dt_names alt_names [descr] sorts
-         induct inject (distinct, distinct, map FewConstrs distinct)
+         induct inject (distinct, distinct, distinct)
  end;
 
 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
   let
     fun constr_of_term (Const (c, T)) = (c, T)

     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
       if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
       else raise exn;
 
     val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
-    val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
+    val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
       DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
         types_syntax constr_syntax (mk_case_names_induct (flat descr));
   in
     derive_datatype_props config dt_names (SOME new_type_names) descr sorts
       induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'

 (** package setup **)
 
 (* setup theory *)
 
 val setup =
-  DatatypeRepProofs.distinctness_limit_setup #>
   simproc_setup #>
   trfun_setup #>
   DatatypeInterpretation.init;
 
 (* outer syntax *)