# HG changeset patch
# User berghofe
# Date 831455892 -7200
# Node ID cbea219f5e5aa9b9208fc756223f945d0e8811cc
# Parent  8b7414384396d97001afa79f62156e4625af3a0a
Added function claset_of.

diff -r 8b7414384396 -r cbea219f5e5a src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Tue May 07 09:53:20 1996 +0200
+++ b/src/HOL/thy_data.ML	Tue May 07 09:58:12 1996 +0200
@@ -11,6 +11,11 @@
       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;
+
 
 (** Information about datatypes **)