# HG changeset patch
# User haftmann
# Date 1257948626 -3600
# Node ID 2640cc1cfc2ed076cb6f8d165fe2d1cca432026f
# Parent  168b928d502403569fc22dc26ae61afa0972d203
adding code equations for constructors

diff -r 168b928d5024 -r 2640cc1cfc2e src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Nov 11 10:06:30 2009 +0100
+++ b/src/HOL/Tools/record.ML	Wed Nov 11 15:10:26 2009 +0100
@@ -1754,11 +1754,12 @@
 
     val ([inject', induct', surjective', split_meta'], thm_thy) =
       defs_thy
-      |> (PureThy.add_thms o map (Thm.no_attributes o apfst Binding.name))
+      |> PureThy.add_thms (map (Thm.no_attributes o apfst Binding.name)
            [("ext_inject", inject),
             ("ext_induct", induct),
             ("ext_surjective", surject),
-            ("ext_split", split_meta)];
+            ("ext_split", split_meta)])
+      ||> Code.add_default_eqn ext_def;
 
   in (thm_thy, extT, induct', inject', split_meta', ext_def) end;