src/HOL/Tools/datatype_hooks.ML

added terminator, named_attribute;

(*  Title:      HOL/Tools/datatype_hooks.ML
    ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen

Hooks for datatype introduction.
*)

signature DATATYPE_HOOKS =
sig
  type hook = string list -> theory -> theory
  val add: hook -> theory -> theory
  val all: hook
end;

structure DatatypeHooks : DATATYPE_HOOKS =
struct

type hook = string list -> theory -> theory;

structure DatatypeHooksData = TheoryDataFun
(
  type T = (serial * hook) list;
  val empty = [];
  val copy = I;
  val extend = I;
  fun merge _ hooks : T = AList.merge (op =) (K true) hooks;
);

fun add hook =
  DatatypeHooksData.map (cons (serial (), hook));

fun all dtcos thy =
  fold (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;

end;