There's no particular reason to duplicate the extension
authorThomas Sewell <tsewell@nicta.com.au>
Fri Sep 11 18:03:30 2009 +1000 (2009-09-11)
changeset 32748887c68b70f7d
parent 32747 8b9ced1051e2
child 32749 3282c12a856c
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.
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Fri Sep 11 15:57:16 2009 +1000
     1.2 +++ b/src/HOL/Tools/record.ML	Fri Sep 11 18:03:30 2009 +1000
     1.3 @@ -1721,8 +1721,7 @@
     1.4             [("ext_inject", inject),
     1.5              ("ext_induct", induct),
     1.6              ("ext_surjective", surject),
     1.7 -            ("ext_split", split_meta),
     1.8 -            ("ext_def", ext_def)]
     1.9 +            ("ext_split", split_meta)]
    1.10  
    1.11    in (thm_thy,extT,induct',inject',split_meta',ext_def')
    1.12    end;