renamed DatatypeHooks.invoke to all

--- a/src/HOL/Tools/datatype_hooks.ML	Wed Nov 08 19:48:35 2006 +0100
+++ b/src/HOL/Tools/datatype_hooks.ML	Wed Nov 08 19:48:36 2006 +0100
@@ -9,7 +9,7 @@
 sig
   type hook = string list -> theory -> theory;
   val add: hook -> theory -> theory;
-  val invoke: hook;
+  val all: hook;
   val setup: theory -> theory;
 end;
 
@@ -43,7 +43,7 @@
 fun add hook =
   DatatypeHooksData.map (map_T (cons (serial (), hook)));
 
-fun invoke dtcos thy =
+fun all dtcos thy =
   fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
 
 

--- a/src/HOL/Tools/datatype_package.ML	Wed Nov 08 19:48:35 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 08 19:48:36 2006 +0100
@@ -733,7 +733,7 @@
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
       |> snd
       |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
-      |> DatatypeHooks.invoke (map fst dt_infos);
+      |> DatatypeHooks.all (map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,
@@ -793,7 +793,7 @@
       |> Theory.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
       |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
-      |> DatatypeHooks.invoke (map fst dt_infos);
+      |> DatatypeHooks.all (map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,
@@ -906,7 +906,7 @@
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
       |> snd
       |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
-      |> DatatypeHooks.invoke (map fst dt_infos);
+      |> DatatypeHooks.all (map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,