--- a/src/HOL/thy_data.ML Fri Apr 03 14:37:48 1998 +0200
+++ b/src/HOL/thy_data.ML Fri Apr 03 14:38:19 1998 +0200
@@ -42,7 +42,7 @@
(* data kind 'datatypes' *)
-val datatypesK = "datatypes";
+val datatypesK = "HOL/datatypes";
exception DatatypeInfo of datatype_info Symtab.table;
local
@@ -79,7 +79,7 @@
(* data kind 'records' *)
-val recordsK = "records";
+val recordsK = "HOL/records";
exception Records of record_info Symtab.table;
--- a/src/Provers/classical.ML Fri Apr 03 14:37:48 1998 +0200
+++ b/src/Provers/classical.ML Fri Apr 03 14:38:19 1998 +0200
@@ -140,7 +140,7 @@
(* data kind claset -- forward declaration *)
-val clasetK = "claset";
+val clasetK = "Provers/claset";
exception ClasetData of object ref;
local
--- a/src/Provers/simplifier.ML Fri Apr 03 14:37:48 1998 +0200
+++ b/src/Provers/simplifier.ML Fri Apr 03 14:38:19 1998 +0200
@@ -250,7 +250,7 @@
(* data kind simpset *)
-val simpsetK = "simpset";
+val simpsetK = "Provers/simpset";
exception SimpsetData of simpset ref;
local