src/HOL/Tools/Datatype/datatype.ML
changeset 32900 dc883c6126d4
parent 32896 99cd75a18b78
child 32904 9d27ebc82700
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 09 13:34:34 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 09 13:34:40 2009 +0200
     1.3 @@ -161,23 +161,9 @@
     1.4  
     1.5  val distinctN = "constr_distinct";
     1.6  
     1.7 -fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
     1.8 -    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
     1.9 -      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.10 -        atac 2, resolve_tac thms 1, etac FalseE 1]))
    1.11 -  | ManyConstrs (thm, simpset) =>
    1.12 -      let
    1.13 -        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    1.14 -          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
    1.15 -            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
    1.16 -      in
    1.17 -        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.18 -        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.19 -          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.20 -          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.21 -          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.22 -          etac FalseE 1]))
    1.23 -      end;
    1.24 +fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t
    1.25 +  (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.26 +    atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1]));
    1.27  
    1.28  fun get_constr thy dtco =
    1.29    get_info thy dtco
    1.30 @@ -408,7 +394,7 @@
    1.31    in
    1.32      thy2
    1.33      |> derive_datatype_props config dt_names alt_names [descr] sorts
    1.34 -         induct inject (distinct, distinct, map FewConstrs distinct)
    1.35 +         induct inject (distinct, distinct, distinct)
    1.36   end;
    1.37  
    1.38  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
    1.39 @@ -545,7 +531,7 @@
    1.40        else raise exn;
    1.41  
    1.42      val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
    1.43 -    val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
    1.44 +    val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
    1.45        DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
    1.46          types_syntax constr_syntax (mk_case_names_induct (flat descr));
    1.47    in
    1.48 @@ -562,7 +548,6 @@
    1.49  (* setup theory *)
    1.50  
    1.51  val setup =
    1.52 -  DatatypeRepProofs.distinctness_limit_setup #>
    1.53    simproc_setup #>
    1.54    trfun_setup #>
    1.55    DatatypeInterpretation.init;