# HG changeset patch
# User Thomas Sewell <tsewell@nicta.com.au>
# Date 1252656210 -36000
# Node ID 887c68b70f7ded7a5e16b82a7a9fa2782f48962e
# Parent  8b9ced1051e256fe26449ca5cf71b65e6db5c133
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.

diff -r 8b9ced1051e2 -r 887c68b70f7d src/HOL/Tools/record.ML
--- 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;