# HG changeset patch
# User berghofe
# Date 870820900 -7200
# Node ID 7e5300420b0314faec2f4ed86cca06980bd0dda3
# Parent  5756c98ebf1fab162ca6528c916edb6929f93fdb
Moved functions from file "thy_data.ML".

diff -r 5756c98ebf1f -r 7e5300420b03 src/FOL/cladata.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
diff -r 5756c98ebf1f -r 7e5300420b03 src/FOL/simpdata.ML
--- 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;