src/FOL/thy_data.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/thy_data.ML	Fri Jan 03 15:01:55 1997 +0100
@@ -0,0 +1,19 @@
+(*  Title:      FOL/thy_data.ML
+    ID:         $Id$
+    Author:     Carsten Clasohm
+    Copyright   1995 TU Muenchen
+
+Definitions that have to be reread after init_thy_reader has been invoked
+*)
+
+fun simpset_of tname =
+  case get_thydata tname "simpset" of
+      None => empty_ss
+    | Some (SS_DATA ss) => ss;
+
+fun claset_of tname =
+  case get_thydata tname "claset" of
+      None => empty_cs
+    | Some (CS_DATA cs) => cs;
+
+