# HG changeset patch
# User haftmann
# Date 1255335847 -7200
# Node ID 9d27ebc827006ac85937478b23df938180a82739
# Parent  793c993c63aa4f0cba73a32214e398e28b03aaf2
dropped redundancy

diff -r 793c993c63aa -r 9d27ebc82700 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 09:25:27 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 10:24:07 2009 +0200
@@ -321,7 +321,7 @@
     split_asm = split_asm});
 
 fun derive_datatype_props config dt_names alt_names descr sorts
-    induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
+    induct inject (distinct_rules, distinct_rewrites) thy1 =
   let
     val thy2 = thy1 |> Theory.checkpoint;
     val flat_descr = flat descr;
@@ -346,7 +346,7 @@
 
     val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
     val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
-      (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
+      (hd descr ~~ inject ~~ distinct_rules ~~ exhaust ~~ nchotomys ~~
         case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
     val dt_names = map fst dt_infos;
     val prfx = Binding.qualify true (space_implode "_" new_type_names);
@@ -394,7 +394,7 @@
   in
     thy2
     |> derive_datatype_props config dt_names alt_names [descr] sorts
-         induct inject (distinct, distinct, distinct)
+         induct inject (distinct, distinct)
  end;
 
 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
@@ -531,12 +531,12 @@
       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), 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'
+      induct inject (distinct_rules, distinct_rewrites) thy'
   end;
 
 val add_datatype = gen_add_datatype cert_typ;
diff -r 793c993c63aa -r 9d27ebc82700 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 12 09:25:27 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Oct 12 10:24:07 2009 +0200
@@ -15,8 +15,7 @@
   val representation_proofs : config -> info Symtab.table ->
     string list -> descr list -> (string * sort) list ->
       (binding * mixfix) list -> (binding * mixfix) list list -> attribute
-        -> theory -> (thm list list * (thm list list * thm list list *
-          thm list list) * thm) * theory
+        -> theory -> (thm list list * (thm list list * thm list list) * thm) * theory
 end;
 
 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -618,7 +617,7 @@
       ||> Theory.checkpoint;
 
   in
-    ((constr_inject', (distinct_thms', dist_rewrites, distinct_thms'), dt_induct'), thy7)
+    ((constr_inject', (distinct_thms', dist_rewrites), dt_induct'), thy7)
   end;
 
 end;