src/HOL/Nominal/nominal_package.ML
changeset 18017 f6abeac6dcb5
parent 18016 8f3a80033ba4
child 18045 6d69a4190eb2
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:22:26 2005 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Oct 28 18:53:26 2005 +0200
     1.3 @@ -1893,11 +1893,11 @@
     1.4              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
     1.5                  (prems ~~ constr_defs))]));
     1.6  
     1.7 -    val case_names_induct = mk_case_names_induct descr;
     1.8 +    val case_names_induct = mk_case_names_induct (List.concat descr');
     1.9  
    1.10      val (thy9, _) = thy8 |>
    1.11        Theory.add_path big_name |>
    1.12 -      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.13 +      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
    1.14        Theory.parent_path |>>>
    1.15        DatatypeAux.store_thmss "distinct" new_type_names distinct_thms |>>>
    1.16        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>