# HG changeset patch
# User wenzelm
# Date 878555360 -3600
# Node ID 6e2d41a5ea43ad9f913865be22a55b0bff3226fe
# Parent  aa29a521e5948bfd10924da4f789c4c778111753
adapted to new implicit claset;

diff -r aa29a521e594 -r 6e2d41a5ea43 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Mon Nov 03 12:07:13 1997 +0100
+++ b/src/HOL/cladata.ML	Mon Nov 03 12:09:20 1997 +0100
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
     Copyright   1996  University of Cambridge
 
-Setting up the classical reasoner 
+Setting up the classical reasoner.
 *)
 
 
@@ -46,25 +46,7 @@
 val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
                      addSEs [exE] 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;
-
-    fun get () = CS_DATA (!claset);
-in add_thydata "HOL"
-     ("claset", ThyMethods {merge = merge, put = put, get = get})
-end;
-
-fun claset_of tname =
-  case get_thydata tname "claset" of
-      None => empty_cs
-    | Some (CS_DATA cs) => cs;
-
-claset := HOL_cs;
+claset_ref() := HOL_cs;
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
 qed_goal "alt_ex1E" thy