renamed DatatypeHooks.invoke to all
authorhaftmann
Wed Nov 08 19:48:36 2006 +0100 (2006-11-08)
changeset 2125194e77628a47d
parent 21250 a268f6288fb6
child 21252 9bffcdfd7553
renamed DatatypeHooks.invoke to all
src/HOL/Tools/datatype_hooks.ML
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_hooks.ML	Wed Nov 08 19:48:35 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_hooks.ML	Wed Nov 08 19:48:36 2006 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    type hook = string list -> theory -> theory;
     1.6    val add: hook -> theory -> theory;
     1.7 -  val invoke: hook;
     1.8 +  val all: hook;
     1.9    val setup: theory -> theory;
    1.10  end;
    1.11  
    1.12 @@ -43,7 +43,7 @@
    1.13  fun add hook =
    1.14    DatatypeHooksData.map (map_T (cons (serial (), hook)));
    1.15  
    1.16 -fun invoke dtcos thy =
    1.17 +fun all dtcos thy =
    1.18    fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    1.19  
    1.20  
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Nov 08 19:48:35 2006 +0100
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 08 19:48:36 2006 +0100
     2.3 @@ -733,7 +733,7 @@
     2.4        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
     2.5        |> snd
     2.6        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
     2.7 -      |> DatatypeHooks.invoke (map fst dt_infos);
     2.8 +      |> DatatypeHooks.all (map fst dt_infos);
     2.9    in
    2.10      ({distinct = distinct,
    2.11        inject = inject,
    2.12 @@ -793,7 +793,7 @@
    2.13        |> Theory.parent_path
    2.14        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    2.15        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    2.16 -      |> DatatypeHooks.invoke (map fst dt_infos);
    2.17 +      |> DatatypeHooks.all (map fst dt_infos);
    2.18    in
    2.19      ({distinct = distinct,
    2.20        inject = inject,
    2.21 @@ -906,7 +906,7 @@
    2.22        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    2.23        |> snd
    2.24        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    2.25 -      |> DatatypeHooks.invoke (map fst dt_infos);
    2.26 +      |> DatatypeHooks.all (map fst dt_infos);
    2.27    in
    2.28      ({distinct = distinct,
    2.29        inject = inject,