# HG changeset patch
# User wenzelm
# Date 878556494 -3600
# Node ID 6fd0f439e50e347f8c166b7b017473c469656f11
# Parent  9e501199ec019e59c65990626ae784604affcbc0
adapted to new implicit claset;

diff -r 9e501199ec01 -r 6fd0f439e50e src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Mon Nov 03 12:28:01 1997 +0100
+++ b/src/FOL/cladata.ML	Mon Nov 03 12:28:14 1997 +0100
@@ -45,26 +45,8 @@
 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
                      addSEs [exE,alt_ex1E] addEs [allE];
 
-
-exception CS_DATA of claset;
-
-let fun merge [] = CS_DATA empty_cs
-      | merge cs = let val cs = map (fn CS_DATA x => x) cs;
-                   in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
-
-    fun put (CS_DATA cs) = claset := cs;
+claset_ref() := FOL_cs;
 
-    fun get () = CS_DATA (!claset);
-in add_thydata "FOL"
-     ("claset", ThyMethods {merge = merge, put = put, get = get})
-end;
-
-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 =