--- 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;