changeset 3610 | 7e5300420b03 |
parent 3566 | c9c351374651 |
child 3835 | 9a5a4e123859 |
--- a/src/FOL/simpdata.ML Wed Aug 06 00:39:13 1997 +0200 +++ b/src/FOL/simpdata.ML Wed Aug 06 00:41:40 1997 +0200 @@ -247,9 +247,10 @@ ("simpset", ThyMethods {merge = merge, put = put, get = get}) end; - -add_thy_reader_file "thy_data.ML"; - +fun simpset_of tname = + case get_thydata tname "simpset" of + None => empty_ss + | Some (SS_DATA ss) => ss;