1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jun 26 16:52:55 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 26 16:53:37 2000 +0200
     1.3 @@ -713,27 +713,28 @@
     1.4            [descr] sorts reccomb_names rec_thms thy8
     1.5        else (thy8, []);
     1.6  
     1.7 -    val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
     1.8 +    val (thy10, [induction']) = thy9 |>
     1.9 +      (#1 o store_thmss "inject" new_type_names inject) |>
    1.10 +      (#1 o store_thmss "distinct" new_type_names distinct) |>
    1.11 +      Theory.add_path (space_implode "_" new_type_names) |>
    1.12 +      PureThy.add_thms [(("induct", induction), [case_names_induct])];
    1.13 +
    1.14 +    val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms)
    1.15        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
    1.16          casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs);
    1.17  
    1.18      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    1.19  
    1.20 -    val (thy10, [induction']) = thy9 |>
    1.21 -      (#1 o store_thmss "inject" new_type_names inject) |>
    1.22 -      (#1 o store_thmss "distinct" new_type_names distinct) |>
    1.23 -      Theory.add_path (space_implode "_" new_type_names) |>
    1.24 -      PureThy.add_thms [(("induct", induction), [case_names_induct])] |>>
    1.25 +    val thy11 = thy10 |>
    1.26        (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.27          (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
    1.28          (("", flat (inject @ distinct)), [iff_add_global]),
    1.29 -        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>>
    1.30 -      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>>
    1.31 -      add_cases_induct dt_infos |>>
    1.32 +        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    1.33 +      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.34 +      add_cases_induct dt_infos |>
    1.35        Theory.parent_path;
    1.36 -
    1.37    in
    1.38 -    (thy10,
    1.39 +    (thy11,
    1.40       {distinct = distinct,
    1.41        inject = inject,
    1.42        exhaustion = casedist_thms,