src/FOL/simpdata.ML
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;