src/HOL/Tools/record.ML
changeset 33595 7264824baf66
parent 33522 737589bb9bb8
child 33612 2640cc1cfc2e
     1.1 --- a/src/HOL/Tools/record.ML	Tue Nov 10 16:11:39 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Nov 10 16:11:43 2009 +0100
     1.3 @@ -150,7 +150,8 @@
     1.4      val thm_thy =
     1.5        cdef_thy
     1.6        |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop (isom_name, istuple))
     1.7 -      |> Sign.parent_path;
     1.8 +      |> Sign.parent_path
     1.9 +      |> Code.add_default_eqn isom_def;
    1.10    in
    1.11      ((isom, cons $ isom), thm_thy)
    1.12    end;