src/HOL/Tools/record_package.ML
changeset 5210 54aaa779b6b4
parent 5201 fac6fea3b782
child 5212 2bc5b5cf0516
--- a/src/HOL/Tools/record_package.ML	Tue Jul 28 17:03:12 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jul 28 17:05:34 1998 +0200
@@ -99,7 +99,7 @@
 
 (* more type class *)
 
-val moreS = ["more"];
+val moreS = ["Record.more"];
 
 
 (* types *)