src/HOL/Tools/record.ML
changeset 32748 887c68b70f7d
parent 32745 192d58483fdf
child 32749 3282c12a856c
     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;