src/HOL/Tools/datatype_hooks.ML
changeset 24626 85eceef2edc7
parent 24625 0398a5e802d3
child 24627 cc6768509ed3
--- a/src/HOL/Tools/datatype_hooks.ML	Tue Sep 18 07:36:38 2007 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  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_rev (fn (_, f) => f dtcos) (DatatypeHooksData.get thy) thy;
-
-end;