1.1 --- a/src/HOL/HOL.ML	Fri Jan 26 20:25:39 1996 +0100
     1.2 +++ b/src/HOL/HOL.ML	Mon Jan 29 13:48:37 1996 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	HOL/hol.ML
     1.5 +(*  Title: 	HOL/HOL.ML
     1.6      ID:         $Id$
     1.7      Author: 	Tobias Nipkow
     1.8      Copyright   1991  University of Cambridge
     1.9 @@ -312,3 +312,35 @@
    1.10  
    1.11  use     "simpdata.ML";
    1.12  simpset := HOL_ss;
    1.13 +
    1.14 +
    1.15 +(** Install simpsets and datatypes in theory structure **)
    1.16 +exception SS_DATA of simpset;
    1.17 +
    1.18 +let fun merge [] = SS_DATA empty_ss
    1.19 +      | merge ss = let val ss = map (fn SS_DATA x => x) ss;
    1.20 +                   in SS_DATA (foldl merge_ss (hd ss, tl ss)) end;
    1.21 +
    1.22 +    fun put (SS_DATA ss) = simpset := ss;
    1.23 +
    1.24 +    fun get () = SS_DATA (!simpset);
    1.25 +in add_thydata HOL.thy
    1.26 +     ("simpset", ThyMethods {merge = merge, put = put, get = get})
    1.27 +end;
    1.28 +
    1.29 +exception DT_DATA of string list;
    1.30 +val datatypes = ref [] : string list ref;
    1.31 +
    1.32 +let fun merge [] = DT_DATA []
    1.33 +      | merge ds = let val ds = map (fn DT_DATA x => x) ds;
    1.34 +                   in DT_DATA (foldl (op union) (hd ds, tl ds)) end;
    1.35 +
    1.36 +    fun put (DT_DATA ds) = datatypes := ds;
    1.37 +
    1.38 +    fun get () = DT_DATA (!datatypes);
    1.39 +in add_thydata HOL.thy
    1.40 +     ("datatypes", ThyMethods {merge = merge, put = put, get = get})
    1.41 +end;
    1.42 +
    1.43 +
    1.44 +add_thy_reader_file "thy_data.ML";