changeset 33173 | b8ca12f6681a |
parent 33171 | 292970b42770 |
child 33278 | ba9f52f56356 |
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Oct 25 20:54:21 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Oct 25 21:35:46 2009 +0100 @@ -321,7 +321,7 @@ fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) ))); val ([def_thm], thy') = thy - |> Sign.declare_const [] decl |> snd + |> Sign.declare_const decl |> snd |> (PureThy.add_defs false o map Thm.no_attributes) [def]; in (defs @ [def_thm], thy')