Implement previous fix (don't duplicate ext_def) correctly.

--- a/src/HOL/Tools/record.ML	Fri Sep 11 18:03:30 2009 +1000
+++ b/src/HOL/Tools/record.ML	Fri Sep 11 20:58:29 2009 +1000
@@ -1714,7 +1714,7 @@
                   asm_simp_tac HOL_ss 1]) end;
     val induct = timeit_msg "record extension induct proof:" induct_prf;
 
-    val ([inject',induct',surjective',split_meta',ext_def'],
+    val ([inject',induct',surjective',split_meta'],
       thm_thy) =
       defs_thy
       |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
@@ -1723,7 +1723,7 @@
             ("ext_surjective", surject),
             ("ext_split", split_meta)]
 
-  in (thm_thy,extT,induct',inject',split_meta',ext_def')
+  in (thm_thy,extT,induct',inject',split_meta',ext_def)
   end;
 
 fun chunks []      []   = []