src/FOL/cladata.ML
changeset 3610 7e5300420b03
parent 2867 0aa5a3cd4550
child 3835 9a5a4e123859
--- a/src/FOL/cladata.ML	Wed Aug 06 00:39:13 1997 +0200
+++ b/src/FOL/cladata.ML	Wed Aug 06 00:41:40 1997 +0200
@@ -61,6 +61,11 @@
 
 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 = 
   struct