# HG changeset patch
# User clasohm
# Date 829305686 -7200
# Node ID a7a6c3fb3cdd3468af9c80c54ad87c4972120af1
# Parent  cbba49da513994a66d75a8f86af567a31c7557b5
changed first parameter of add_thydata and get_thydata

diff -r cbba49da5139 -r a7a6c3fb3cdd src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Thu Apr 11 13:41:22 1996 +0200
+++ b/src/HOL/HOL.ML	Fri Apr 12 12:41:26 1996 +0200
@@ -357,7 +357,7 @@
     fun put (SS_DATA ss) = simpset := ss;
 
     fun get () = SS_DATA (!simpset);
-in add_thydata HOL.thy
+in add_thydata "HOL"
      ("simpset", ThyMethods {merge = merge, put = put, get = get})
 end;
 
@@ -371,7 +371,7 @@
     fun put (DT_DATA ds) = datatypes := ds;
 
     fun get () = DT_DATA (!datatypes);
-in add_thydata HOL.thy
+in add_thydata "HOL"
      ("datatypes", ThyMethods {merge = merge, put = put, get = get})
 end;
 
diff -r cbba49da5139 -r a7a6c3fb3cdd src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Thu Apr 11 13:41:22 1996 +0200
+++ b/src/HOL/thy_data.ML	Fri Apr 12 12:41:26 1996 +0200
@@ -7,11 +7,11 @@
 *)
 
 fun simpset_of tname =
-  case get_thydata (theory_of tname) "simpset" of
+  case get_thydata tname "simpset" of
       None => empty_ss
     | Some (SS_DATA ss) => ss;
 
 fun datatypes_of tname =
-  case get_thydata (theory_of tname) "datatypes" of
+  case get_thydata tname "datatypes" of
       None => []
     | Some (DT_DATA ds) => ds;