# HG changeset patch
# User berghofe
# Date 870821065 -7200
# Node ID 3199f744cf4f8ea2da3d82144b551203a997a2b6
# Parent  7e5300420b0314faec2f4ed86cca06980bd0dda3
The functions in this file have been moved to "cladata.ML"
and "simpdata.ML".

diff -r 7e5300420b03 -r 3199f744cf4f 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;
-
-