--- 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;
--- 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;