# HG changeset patch
# User Thomas Sewell <tsewell@nicta.com.au>
# Date 1252666709 -36000
# Node ID 3282c12a856cd45d9d9d71d24cbbe0b539480b82
# Parent  887c68b70f7ded7a5e16b82a7a9fa2782f48962e
Implement previous fix (don't duplicate ext_def) correctly.

diff -r 887c68b70f7d -r 3282c12a856c src/HOL/Tools/record.ML
--- 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 []      []   = []