src/HOL/simpdata.ML

--- a/src/HOL/simpdata.ML	Wed Aug 06 01:12:03 1997 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 06 01:13:46 1997 +0200
@@ -401,6 +401,11 @@
      ("simpset", ThyMethods {merge = merge, put = put, get = get})
 end;
 
+fun simpset_of tname =
+  case get_thydata tname "simpset" of
+      None => empty_ss
+    | Some (SS_DATA ss) => ss;
+
 type dtype_info = {case_const:term,
                    case_rewrites:thm list,
                    constructors:term list,
@@ -426,10 +431,6 @@
 end;
 
 
-add_thy_reader_file "thy_data.ML";
-
-
-
 
 (*** Integration of simplifier with classical reasoner ***)