src/HOL/Tools/datatype_hooks.ML
changeset 20177 0af885e3dabf
parent 19935 604c203beb3a
child 21251 94e77628a47d
     1.1 --- a/src/HOL/Tools/datatype_hooks.ML	Fri Jul 21 14:46:27 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_hooks.ML	Fri Jul 21 14:47:22 2006 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature DATATYPE_HOOKS =
     1.6  sig
     1.7 -  type hook = string -> theory -> theory;
     1.8 +  type hook = string list -> theory -> theory;
     1.9    val add: hook -> theory -> theory;
    1.10    val invoke: hook;
    1.11    val setup: theory -> theory;
    1.12 @@ -19,7 +19,7 @@
    1.13  
    1.14  (* theory data *)
    1.15  
    1.16 -type hook = string -> theory -> theory;
    1.17 +type hook = string list -> theory -> theory;
    1.18  datatype T = T of (serial * hook) list;
    1.19  
    1.20  fun map_T f (T hooks) = T (f hooks);
    1.21 @@ -43,8 +43,8 @@
    1.22  fun add hook =
    1.23    DatatypeHooksData.map (map_T (cons (serial (), hook)));
    1.24  
    1.25 -fun invoke dtco thy =
    1.26 -  fold (fn (_, f) => f dtco) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    1.27 +fun invoke dtcos thy =
    1.28 +  fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    1.29  
    1.30  
    1.31  (* theory setup *)