src/HOL/cladata.ML

--- a/src/HOL/cladata.ML	Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/cladata.ML	Wed Aug 06 01:13:46 1997 +0200
@@ -59,6 +59,11 @@
      ("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;
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)