src/HOL/Tools/Datatype/datatype.ML
changeset 32907 0300f8dd63ea
parent 32904 9d27ebc82700
child 32911 5f7386f7cbe6
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 11:03:10 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 13:40:28 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) thy1 =
     1.8 +    induct inject distinct thy1 =
     1.9    let
    1.10      val thy2 = thy1 |> Theory.checkpoint;
    1.11      val flat_descr = flat descr;
    1.12 @@ -334,7 +334,7 @@
    1.13        descr sorts exhaust thy3;
    1.14      val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
    1.15        config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
    1.16 -      inject distinct_rewrites (Simplifier.theory_context thy4 dist_ss) induct thy4;
    1.17 +      inject distinct (Simplifier.theory_context thy4 dist_ss) induct thy4;
    1.18      val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
    1.19        config new_type_names descr sorts rec_names rec_rewrites thy5;
    1.20      val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
    1.21 @@ -342,15 +342,15 @@
    1.22      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    1.23        descr sorts thy7;
    1.24      val (splits, thy9) = DatatypeAbsProofs.prove_split_thms
    1.25 -      config new_type_names descr sorts inject distinct_rewrites exhaust case_rewrites thy8;
    1.26 +      config new_type_names descr sorts inject distinct exhaust case_rewrites thy8;
    1.27  
    1.28      val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
    1.29      val dt_infos = map_index (make_dt_info alt_names flat_descr sorts induct inducts rec_names rec_rewrites)
    1.30 -      (hd descr ~~ inject ~~ distinct_rules ~~ exhaust ~~ nchotomys ~~
    1.31 +      (hd descr ~~ inject ~~ distinct ~~ exhaust ~~ nchotomys ~~
    1.32          case_names ~~ case_rewrites ~~ case_congs ~~ weak_case_congs ~~ splits);
    1.33      val dt_names = map fst dt_infos;
    1.34      val prfx = Binding.qualify true (space_implode "_" new_type_names);
    1.35 -    val simps = flat (inject @ distinct_rules @ case_rewrites) @ rec_rewrites;
    1.36 +    val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
    1.37      val named_rules = flat (map_index (fn (index, tname) =>
    1.38        [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
    1.39         ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
    1.40 @@ -362,11 +362,11 @@
    1.41      |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
    1.42          ((prfx (Binding.name "inducts"), inducts), []),
    1.43          ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
    1.44 -        ((Binding.empty, flat case_rewrites @ flat distinct_rules @ rec_rewrites),
    1.45 +        ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
    1.46            [Simplifier.simp_add]),
    1.47          ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
    1.48          ((Binding.empty, flat inject), [iff_add]),
    1.49 -        ((Binding.empty, map (fn th => th RS notE) (flat distinct_rules)),
    1.50 +        ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
    1.51            [Classical.safe_elim NONE]),
    1.52          ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
    1.53          @ named_rules @ unnamed_rules)
    1.54 @@ -394,7 +394,7 @@
    1.55    in
    1.56      thy2
    1.57      |> derive_datatype_props config dt_names alt_names [descr] sorts
    1.58 -         induct inject (distinct, distinct)
    1.59 +         induct inject distinct
    1.60   end;
    1.61  
    1.62  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
    1.63 @@ -531,12 +531,12 @@
    1.64        else raise exn;
    1.65  
    1.66      val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
    1.67 -    val ((inject, (distinct_rules, distinct_rewrites), induct), thy') = thy |>
    1.68 +    val ((inject, distinct, induct), thy') = thy |>
    1.69        DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
    1.70          types_syntax constr_syntax (mk_case_names_induct (flat descr));
    1.71    in
    1.72      derive_datatype_props config dt_names (SOME new_type_names) descr sorts
    1.73 -      induct inject (distinct_rules, distinct_rewrites) thy'
    1.74 +      induct inject distinct thy'
    1.75    end;
    1.76  
    1.77  val add_datatype = gen_add_datatype cert_typ;