| changeset 38531 | a11a1e4e0403 |
| parent 38530 | 048338a9b389 |
| child 38533 | 8d23c7403699 |
--- 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";