src/HOL/Tools/Datatype/datatype.ML
changeset 32904 9d27ebc82700
parent 32900 dc883c6126d4
child 32907 0300f8dd63ea
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 09:25:27 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 10:24:07 2009 +0200
     1.3 @@ -321,7 +321,7 @@
     1.4      split_asm = split_asm});
     1.5  
     1.6  fun derive_datatype_props config dt_names alt_names descr sorts
     1.7 -    induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy1 =
     1.8 +    induct inject (distinct_rules, distinct_rewrites) thy1 =
     1.9    let
    1.10      val thy2 = thy1 |> Theory.checkpoint;
    1.11      val flat_descr = flat descr;
    1.12 @@ -346,7 +346,7 @@
    1.13  
    1.14      val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.15      val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
    1.16 -      (hd descr ~~ inject ~~ distinct_entry ~~ exhaust ~~ nchotomys ~~
    1.17 +      (hd descr ~~ inject ~~ distinct_rules ~~ exhaust ~~ nchotomys ~~
    1.18          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
    1.19      val dt_names = map fst dt_infos;
    1.20      val prfx = Binding.qualify true (space_implode "_" new_type_names);
    1.21 @@ -394,7 +394,7 @@
    1.22    in
    1.23      thy2
    1.24      |> derive_datatype_props config dt_names alt_names [descr] sorts
    1.25 -         induct inject (distinct, distinct, distinct)
    1.26 +         induct inject (distinct, distinct)
    1.27   end;
    1.28  
    1.29  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
    1.30 @@ -531,12 +531,12 @@
    1.31        else raise exn;
    1.32  
    1.33      val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
    1.34 -    val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
    1.35 +    val ((inject, (distinct_rules, distinct_rewrites), induct), thy') = thy |>
    1.36        DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
    1.37          types_syntax constr_syntax (mk_case_names_induct (flat descr));
    1.38    in
    1.39      derive_datatype_props config dt_names (SOME new_type_names) descr sorts
    1.40 -      induct inject (distinct_rules, distinct_rewrites, distinct_entry) thy'
    1.41 +      induct inject (distinct_rules, distinct_rewrites) thy'
    1.42    end;
    1.43  
    1.44  val add_datatype = gen_add_datatype cert_typ;