src/HOL/Tools/record.ML

--- a/src/HOL/Tools/record.ML	Tue Nov 10 16:11:39 2009 +0100
+++ b/src/HOL/Tools/record.ML	Tue Nov 10 16:11:43 2009 +0100
@@ -150,7 +150,8 @@
     val thm_thy =
       cdef_thy
       |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
-      |> Sign.parent_path;
+      |> Sign.parent_path
+      |> Code.add_default_eqn isom_def;
   in
     ((isom, cons $ isom), thm_thy)
   end;