--- a/src/HOL/thy_data.ML Fri Jul 24 13:00:36 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: HOL/thy_data.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-HOL theory data: datatypes.
-*)
-
-type datatype_info =
- {case_const: term,
- case_rewrites: thm list,
- constructors: term list,
- induct_tac: string -> int -> tactic,
- nchotomy: thm,
- exhaustion: thm,
- exhaust_tac: string -> int -> tactic,
- case_cong: thm};
-
-
-signature THY_DATA =
-sig
- val get_datatypes_sg: Sign.sg -> datatype_info Symtab.table
- val get_datatypes: theory -> datatype_info Symtab.table
- val put_datatypes: datatype_info Symtab.table -> theory -> theory
- val setup: (theory -> theory) list
-end;
-
-structure ThyData: THY_DATA =
-struct
-
-
-(* data kind 'HOL/datatypes' *)
-
-structure DatatypesArgs =
-struct
- val name = "HOL/datatypes";
- type T = datatype_info Symtab.table;
-
- val empty = Symtab.empty;
- val prep_ext = I;
- val merge: T * T -> T = Symtab.merge (K true);
-
- fun print sg tab =
- Pretty.writeln (Pretty.strs ("datatypes:" ::
- map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
-end;
-
-structure DatatypesData = TheoryDataFun(DatatypesArgs);
-val get_datatypes_sg = DatatypesData.get_sg;
-val get_datatypes = DatatypesData.get;
-val put_datatypes = DatatypesData.put;
-
-
-(* setup *)
-
-val setup = [DatatypesData.init];
-
-
-end;