src/HOL/Tools/datatype_package.ML
changeset 21251 94e77628a47d
parent 21243 afffe1f72143
child 21253 f1e3967d559a
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Nov 08 19:48:35 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 08 19:48:36 2006 +0100
     1.3 @@ -733,7 +733,7 @@
     1.4        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
     1.5        |> snd
     1.6        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
     1.7 -      |> DatatypeHooks.invoke (map fst dt_infos);
     1.8 +      |> DatatypeHooks.all (map fst dt_infos);
     1.9    in
    1.10      ({distinct = distinct,
    1.11        inject = inject,
    1.12 @@ -793,7 +793,7 @@
    1.13        |> Theory.parent_path
    1.14        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.15        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.16 -      |> DatatypeHooks.invoke (map fst dt_infos);
    1.17 +      |> DatatypeHooks.all (map fst dt_infos);
    1.18    in
    1.19      ({distinct = distinct,
    1.20        inject = inject,
    1.21 @@ -906,7 +906,7 @@
    1.22        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.23        |> snd
    1.24        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    1.25 -      |> DatatypeHooks.invoke (map fst dt_infos);
    1.26 +      |> DatatypeHooks.all (map fst dt_infos);
    1.27    in
    1.28      ({distinct = distinct,
    1.29        inject = inject,