# HG changeset patch
# User wenzelm
# Date 878646913 -3600
# Node ID de6e388f3d8692e37e4dba8597b5925797b867c3
# Parent  4e75435b01e54dd130887f71e1e786ecf2e8194d
removed old datatype_info;

diff -r 4e75435b01e5 -r de6e388f3d86 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Nov 04 13:31:14 1997 +0100
+++ b/src/HOL/simpdata.ML	Tue Nov 04 13:35:13 1997 +0100
@@ -444,39 +444,11 @@
     Simp_tac i;
 
 
-
-
-(*** Install simpsets and datatypes in theory structure ***)
+(* install implicit simpset *)
 
 simpset_ref() := HOL_ss;
 
 
-type dtype_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};
-
-exception DT_DATA of (string * dtype_info) list;
-val datatypes = ref [] : (string * dtype_info) list ref;
-
-let fun merge [] = DT_DATA []
-      | merge ds =
-          let val ds = map (fn DT_DATA x => x) ds;
-          in DT_DATA (foldl (gen_union eq_fst) (hd ds, tl ds)) end;
-
-    fun put (DT_DATA ds) = datatypes := ds;
-
-    fun get () = DT_DATA (!datatypes);
-in add_thydata "HOL"
-     ("datatypes", ThyMethods {merge = merge, put = put, get = get})
-end;
-
-
-
 (*** Integration of simplifier with classical reasoner ***)
 
 (* rot_eq_tac rotates the first equality premise of subgoal i to the front,