changed the way simpsets and information about datatypes are stored

--- a/src/HOL/HOL.ML	Fri Jan 26 20:25:39 1996 +0100
+++ b/src/HOL/HOL.ML	Mon Jan 29 13:48:37 1996 +0100
@@ -1,4 +1,4 @@
-(*  Title: 	HOL/hol.ML
+(*  Title: 	HOL/HOL.ML
     ID:         $Id$
     Author: 	Tobias Nipkow
     Copyright   1991  University of Cambridge
@@ -312,3 +312,35 @@
 
 use     "simpdata.ML";
 simpset := HOL_ss;
+
+
+(** Install simpsets and datatypes in theory structure **)
+exception SS_DATA of simpset;
+
+let fun merge [] = SS_DATA empty_ss
+      | merge ss = let val ss = map (fn SS_DATA x => x) ss;
+                   in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
+
+    fun put (SS_DATA ss) = simpset := ss;
+
+    fun get () = SS_DATA (!simpset);
+in add_thydata HOL.thy
+     ("simpset", ThyMethods {merge = merge, put = put, get = get})
+end;
+
+exception DT_DATA of string list;
+val datatypes = ref [] : string list ref;
+
+let fun merge [] = DT_DATA []
+      | merge ds = let val ds = map (fn DT_DATA x => x) ds;
+                   in DT_DATA (foldl (op union) (hd ds, tl ds)) end;
+
+    fun put (DT_DATA ds) = datatypes := ds;
+
+    fun get () = DT_DATA (!datatypes);
+in add_thydata HOL.thy
+     ("datatypes", ThyMethods {merge = merge, put = put, get = get})
+end;
+
+
+add_thy_reader_file "thy_data.ML";

--- a/src/HOL/datatype.ML	Fri Jan 26 20:25:39 1996 +0100
+++ b/src/HOL/datatype.ML	Mon Jan 29 13:48:37 1996 +0100
@@ -405,7 +405,7 @@
 	end;
 
     in
-      store_datatype (tname, map (fn (x,_,_) => x) cons_list');
+      datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes);
       (thy |> add_types types
            |> add_arities arities
            |> add_consts consts

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/thy_data.ML	Mon Jan 29 13:48:37 1996 +0100
@@ -0,0 +1,17 @@
+(*  Title: 	HOL/thy_data.ML
+    ID:         $Id$
+    Author: 	Carsten Clasohm
+    Copyright   1995 TU Muenchen
+
+Definitions that have to be reread after init_thy_reader has been invoked
+*)
+
+fun simpset_of tname =
+  case get_thydata (theory_of tname) "simpset" of
+      None => empty_ss
+    | Some (SS_DATA ss) => ss;
+
+fun datatypes_of tname =
+  case get_thydata (theory_of tname) "datatypes" of
+      None => []
+    | Some (DT_DATA ds) => ds;