# HG changeset patch
# User haftmann
# Date 1282051781 -7200
# Node ID a11a1e4e0403dbf004d3c38932cd8c75d74c99a7
# Parent  048338a9b389e6bc00efd3684d35423fbcb06563
authentic syntax allows simplification of type names

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";