Moved functions from file "thy_data.ML".
--- a/src/FOL/cladata.ML Wed Aug 06 00:39:13 1997 +0200
+++ b/src/FOL/cladata.ML Wed Aug 06 00:41:40 1997 +0200
@@ -61,6 +61,11 @@
claset := FOL_cs;
+fun claset_of tname =
+ case get_thydata tname "claset" of
+ None => empty_cs
+ | Some (CS_DATA cs) => cs;
+
(*** Applying BlastFun to create Blast_tac ***)
structure Blast_Data =
struct
--- 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;