src/FOL/simpdata.ML

     fun get () = SS_DATA (!simpset);
 in add_thydata "FOL"
      ("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;
 
 
 
 (*** Integration of simplifier with classical reasoner ***)