src/HOL/Tools/record.ML

       defs_thy
       |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
            [("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;
 
 fun chunks []      []   = []