There's no particular reason to duplicate the extension
constant's definition under the name "ext_def", and it
also prevents you having a field called ext.

--- a/src/HOL/Tools/record.ML	Fri Sep 11 15:57:16 2009 +1000
+++ b/src/HOL/Tools/record.ML	Fri Sep 11 18:03:30 2009 +1000
@@ -1721,8 +1721,7 @@
            [("ext_inject", inject),
             ("ext_induct", induct),
             ("ext_surjective", surject),
-            ("ext_split", split_meta),
-            ("ext_def", ext_def)]
+            ("ext_split", split_meta)]
 
   in (thm_thy,extT,induct',inject',split_meta',ext_def')
   end;