src/HOL/Tools/datatype_hooks.ML
changeset 21251 94e77628a47d
parent 20177 0af885e3dabf
child 22846 fb79144af9a3
     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