diff -r 048338a9b389 -r a11a1e4e0403 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Aug 17 15:19:37 2010 +0200
+++ b/src/HOL/Tools/record.ML	Tue Aug 17 15:29:41 2010 +0200
@@ -298,8 +298,8 @@
 val wN = "w";
 val moreN = "more";
 val schemeN = "_scheme";
-val ext_typeN = "_ext_type";
-val inner_typeN = "_inner_type";
+val ext_typeN = "_ext";
+val inner_typeN = "_inner";
 val extN ="_ext";
 val updateN = "_update";
 val makeN = "make";