The functions in this file have been moved to "cladata.ML"
authorberghofe
Wed, 06 Aug 1997 00:44:25 +0200
changeset 3611 3199f744cf4f
parent 3610 7e5300420b03
child 3612 403db95b54ff
The functions in this file have been moved to "cladata.ML" and "simpdata.ML".
src/FOL/thy_data.ML
--- a/src/FOL/thy_data.ML	Wed Aug 06 00:41:40 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  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;
-
-