# HG changeset patch
# User berghofe
# Date 831455600 -7200
# Node ID 8b7414384396d97001afa79f62156e4625af3a0a
# Parent  bb02e6976258041680cd2d1e4dc7086c02d340e4
Added function for storing default claset in theory.

diff -r bb02e6976258 -r 8b7414384396 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Tue May 07 09:46:25 1996 +0200
+++ b/src/HOL/HOL.ML	Tue May 07 09:53:20 1996 +0200
@@ -387,6 +387,20 @@
 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                      addSEs [exE,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;
+
+    fun get () = CS_DATA (!claset);
+in add_thydata "HOL"
+     ("claset", ThyMethods {merge = merge, put = put, get = get})
+end;
+
+claset := HOL_cs;
 
 section "Simplifier";
 
@@ -408,7 +422,6 @@
      ("simpset", ThyMethods {merge = merge, put = put, get = get})
 end;
 
-
 type dtype_info = {case_const:term, case_rewrites:thm list,
                    constructors:term list, nchotomy:thm, case_cong:thm};