# HG changeset patch
# User wenzelm
# Date 891607099 -7200
# Node ID 06556ca5036d509136236683bb76cd657d0de02f
# Parent  ca29125de4af3df1ec62dc630ec13eecf4f84810
tuned names;

diff -r ca29125de4af -r 06556ca5036d src/HOL/thy_data.ML
--- 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;
 
 
diff -r ca29125de4af -r 06556ca5036d src/Provers/classical.ML
--- 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
diff -r ca29125de4af -r 06556ca5036d src/Provers/simplifier.ML
--- 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